# HG changeset patch # User paulson # Date 995903107 -7200 # Node ID b24017251fc1166c728aaae6f7f5e3b608a3ecb4 # Parent 77ed7e2b56c8c0b661fb27719b22e1a32f1cac2f live links diff -r 77ed7e2b56c8 -r b24017251fc1 src/HOL/ex/README.html --- a/src/HOL/ex/README.html Mon Jul 23 17:37:29 2001 +0200 +++ b/src/HOL/ex/README.html Mon Jul 23 17:45:07 2001 +0200 @@ -7,31 +7,29 @@ features of Isabelle/HOL.

Files cla.ML demonstrates the +
File cla.ML demonstrates the power of Isabelle's classical reasoner. -
Files meson.ML and mesontest.ML present an +
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 +
InSort and Qsort are correctness proofs for sorting functions. -
Primes is a theory of the divides relation, the -greatest common divisor and Euclid's algorithm. +
Primrec proves that Ackermann's +function is not primitive recursive. -
Fib proves some theorems (some rather difficult) about the -Fibonacci function. - -
Tarski is a proof of Tarski's fixedpoint theorem: the full +
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. +
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 +
MT is a preliminary version of Jacob Frost's coinduction example. The full version is on the directory ZF/Coind.