Constructive Rewriting

The subject of this paper is rewriting in an LCF-like general theorem proving framework. It is shown how rewriting of both terms and formulae can be implemented by simple tactics in the generic theorem prover Isabelle. These tactics can easily be combined with induction to yield powerful theorem pro... View More