src/HOL/ex/README.html
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 3279 815ef5848324
child 7146 3c664fbb2910
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
     1 <!-- $Id$ -->
     2 <HTML><HEAD><TITLE>HOL/ex/README</TITLE></HEAD><BODY>
     3 
     4 <H2>ex--Miscellaneous Examples</H2>
     5 
     6 <P>This directory presents a number of small examples, illustrating various
     7 features of Isabelle/HOL.
     8 
     9 <UL> 
    10 <LI>Files <KBD>cla.ML</KBD> demonstrates the
    11 power of Isabelle's classical reasoner.
    12 
    13 <LI>Files <KBD>meson.ML</KBD> and <KBD>mesontest.ML</KBD> present an
    14 implementation of the Model Elimination (ME) proof procedure, which is even
    15 more powerful than the classical reasoner but not generic.
    16 
    17 <LI><KBD>InSort</KBD> and <KBD>Qsort</KBD> are correctness proofs for sorting
    18 functions.
    19 
    20 <LI><KBD>Primes</KBD> is a theory of the <EM>divides</EM> relation, the
    21 greatest common divisor and Euclid's algorithm.
    22 
    23 <LI><KBD>NatSum</KBD> demonstrates the power of permutative rewriting.
    24 Well-known identities about summations are proved using just induction and
    25 rewriting.
    26 
    27 <LI><KBD>MT</KBD> is a preliminary version of Jacob Frost's coinduction
    28 example.  The full version is on the directory <KBD>ZF/Coind</KBD>.
    29 </UL>
    30 
    31 <HR>
    32 <P>Last modified 6 May 1997
    33 
    34 <ADDRESS>
    35 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    36 </ADDRESS>
    37 </BODY></HTML>