# HG changeset patch
# User paulson
# Date 863005818 -7200
# Node ID f58719b49cae37bc49aeb77df9e88de67fcf4f7f
# Parent 2fe26ca380a1ce87f99eba64b6253b7537426ad5
Documentation for directory "ex"
diff -r 2fe26ca380a1 -r f58719b49cae src/HOL/ex/README.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/README.html Wed May 07 13:50:18 1997 +0200
@@ -0,0 +1,37 @@
+
+HOL/ex/ReadMe
+
+ex--Miscellaneous Examples
+
+This directory presents a number of small examples, illustrating various
+features of Isabelle/HOL.
+
+
+- Files cla.ML demonstrates the
+power of Isabelle's classical reasoner.
+
+
- Files meson.ML and mesontest.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.
+
+
- Primes is a theory of the divides relation, the
+greatest common divisor and Euclid's algorithm.
+
+
- 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 6 May 1997
+
+
+lcp@cl.cam.ac.uk
+
+