Term rewriting and beyond — theorem proving in Isabelle

The subject of this paper is theorem proving based on rewriting and induction. Both principles are implemented as tactics within the generic theorem prover Isabelle. Isabelle's higher-order features enable us to go beyond first-order rewriting and express rewriting with conditionals, induction schemata, higher-order functions and program transformers. Applications include the verification and transformation of functional versions of insertion sort and quicksort.