src/HOL/ex/README.html
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 15582 7219facb3fd0
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <!-- $Id$ -->
     4 
     5 <HTML>
     6 
     7 <HEAD>
     8   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     9   <TITLE>HOL/ex/README</TITLE>
    10 </HEAD>
    11 
    12 <BODY>
    13 
    14 <H2>ex--Miscellaneous Examples</H2>
    15 
    16 <P>This directory presents a number of small examples, illustrating various
    17 features of Isabelle/HOL.
    18 
    19 <UL> 
    20 <LI><A HREF="Classical.thy"><KBD>Classical</KBD></A> demonstrates the power 
    21 of Isabelle's classical reasoner.
    22 
    23 <LI>Files <A HREF="mesontest.ML"><KBD>mesontest.ML</KBD></A> and
    24 <A HREF="mesontest2.ML"><KBD>mesontest2.ML</KBD></A> present an
    25 implementation of the Model Elimination (ME) proof procedure, which is even
    26 more powerful than the classical reasoner but not generic.
    27 
    28 <LI><A HREF="InSort.thy"><KBD>InSort</KBD></A> and <A HREF="Qsort.thy"><KBD>Qsort</KBD></A> are correctness proofs for sorting
    29 functions.
    30 
    31 <LI><A HREF="Primrec.thy"><KBD>Primrec</KBD></A> proves that Ackermann's
    32 function is not primitive recursive.
    33 
    34 <LI><A HREF="Tarski.thy"><KBD>Tarski</KBD></A> is a proof of Tarski's fixedpoint theorem: the full
    35 version, which states that the fixedpoints of a complete lattice themselves
    36 form a complete lattice.  The example demonstrates first-class reasoning about theories.
    37 
    38 <LI><A HREF="NatSum.thy"><KBD>NatSum</KBD></A> demonstrates the power of permutative rewriting.
    39 Well-known identities about summations are proved using just induction and
    40 rewriting.
    41 
    42 <LI><A HREF="MT.thy"><KBD>MT</KBD></A> is a preliminary version of Jacob Frost's coinduction
    43 example.  The full version is on the directory <KBD>ZF/Coind</KBD>.
    44 </UL>
    45 
    46 <HR>
    47 <P>Last modified on $Date$
    48 
    49 <ADDRESS>
    50 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    51 </ADDRESS>
    52 </BODY>
    53 </HTML>