# HG changeset patch
# User paulson
# Date 1280228530 -3600
# Node ID ada7d21fde114f151149845752898723f327574e
# Parent a79abb22ca9c46a4e7e9d7a8977233255b5b0096
Deleted an obsolete file
diff -r a79abb22ca9c -r ada7d21fde11 src/HOL/ex/README.html
--- a/src/HOL/ex/README.html Mon Jul 26 18:25:19 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-
-
-
-
-
-
-
-
- HOL/ex/README
-
-
-
-
-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
-
-
-