A higher-order implementation of rewriting (Q800739): Difference between revisions

This paper describes the implementation of rewriting in LCF (the interactive theorem-prover for Scott's logic of computable functions). Because many theorem-proving tools are written in ML (the metalanguage for LCF) an introduction into ML is presented. Further sections contain detailed descriptions of pattern matching primitives, term conversions, formula conversions and rewriting tactics. Good examples and clear style make the paper very readable.