## ex--Miscellaneous Examples

This directory presents a number of small examples, illustrating various
features of Isabelle/HOL.

`Classical` demonstrates the power
of Isabelle's classical reasoner.
- Files
`mesontest.ML` and
`mesontest2.ML` present an
implementation of the Model Elimination (ME) proof procedure, which is even
more powerful than the classical reasoner but not generic.
`InSort` and `Qsort` are correctness proofs for sorting
functions.
`Primrec` proves that Ackermann's
function is not primitive recursive.
`Tarski` is a proof of Tarski's fixedpoint theorem: the full
version, which states that the fixedpoints of a complete lattice themselves
form a complete lattice. The example demonstrates first-class reasoning about theories.
`NatSum` demonstrates the power of permutative rewriting.
Well-known identities about summations are proved using just induction and
rewriting.
`MT` is a preliminary version of Jacob Frost's coinduction
example. The full version is on the directory `ZF/Coind`.

Last modified on $Date$

lcp@cl.cam.ac.uk