Admin/page/main-content/index.content
author kleing
Tue Aug 17 10:49:52 2004 +0200 (2004-08-17)
changeset 15138 9390018ea712
parent 15137 8a17799687e7
child 15276 0c1d03e37881
permissions -rw-r--r--
improved wording course material
     1 %title%
     2 Isabelle
     3 
     4 %body%
     5 
     6 <p>
     7 
     8 <h2>What is Isabelle?</h2>
     9 
    10 Isabelle is a popular generic theorem proving environment developed at
    11 Cambridge University (<a
    12 href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
    13 Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
    14 See the <a href="overview.html">Isabelle overview</a>.
    15 
    16 <p>
    17 
    18 These pages provide general information on Isabelle, more specific
    19 information is available from the local pages
    20 
    21 <ul>
    22 
    23 <li><a
    24 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
    25 at Cambridge</strong></a>
    26 
    27 <li><a href="http://www4.in.tum.de/proj/theoremprov/group.html"><strong>Isabelle
    28 at Munich</strong></a>
    29 
    30 </ul>
    31 
    32 See there for information on projects done with Isabelle, mailing list
    33 archives, research papers, the Isabelle bibliography, and Isabelle
    34 workshops and courses.
    35 
    36 <p>
    37 
    38 <h2>Course Material</h2>
    39 
    40 The <a
    41 href="http://isabelle.in.tum.de/coursematerial/">course material</a>
    42 page makes slides, demos, and exercises of a growing number of
    43 Isabelle courses available. It is meant as a resource for people 
    44 who would like to learn Isabelle as well as for those who would like 
    45 to teach it.
    46 
    47 <p>
    48 
    49 <h2>AFP - The Archive of Formal Proofs</h2>
    50 
    51 The <a href="http://afp.sf.net">Archive of Formal Proofs</a> is a
    52 collection of proof libraries, examples, and larger scientifc
    53 developments, mechanically checked in Isabelle. It is organized in the
    54 way of a scientific journal. Submissions are refereed.
    55 
    56 <p>
    57 
    58 <h2><!-- _GP_ distname --></h2>
    59 New features in <strong><!-- _GP_ distname --></strong> include
    60 <ul>
    61 <li>New image HOL4 with imported library from HOL4 system on top of
    62   HOL-Complex (about 2500 additional theorems).</li>
    63 
    64 <li>New theory Ring_and_Field with over 250 basic numerical laws, 
    65   all proved in axiomatic type classes for semirings, rings and fields.</li>
    66 
    67 <li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li>
    68 
    69 <li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>
    70 
    71 <li>New theory of matrices with an application to linear programming in HOL-Matrix.</li>
    72 
    73 <li>Improved locales (named proof contexts), instantiation of locales.</li>
    74 
    75 <li>Improved handling of linear and partial orders in simplifier.</li>
    76  
    77 <li>New <code>specification</code> command for definition by specification.</li>  
    78 
    79 <li>New Isar command <code>finalconsts</code> prevents constants being given a definition later.</li>  
    80 
    81 <li><code>arith</code> now generates counterexamples for reals as well.</li>
    82 
    83 <li>New <code>quickcheck</code> command
    84     to search for counterexamples of executable goals.
    85   (see HOL/ex/Quickcheck_Examples.thy)</li>
    86 <li>New <code>refute</code> command
    87     to search for finite countermodels of goals.
    88   (see HOL/ex/Refute_Examples.thy)
    89 </li>
    90 
    91 <li>Presentation and x-symbol enhancements, greek letters and
    92 sub/superscripts allowed in identifiers.</li>
    93 </ul>
    94 <a href="dist/<!-- _GP_ distname -->/NEWS">[Complete Changelog]</a>
    95 <p>
    96 The <strong><!-- _GP_ distname --></strong> distribution is available
    97 from several <a href="dist/index.html">mirror sites</a>.  It includes
    98 source and binary packages and browsable documentation. You can also
    99 browse the <a href="library/index.html">Isabelle theory library</a>
   100 online. For the curious, there is a nightly generated <a
   101 href="http://isabelle.in.tum.de/devel/">development snapshot</a>
   102 available.
   103 
   104 <p>
   105 
   106 <h2>Mailing list</h2>
   107 
   108 Use the mailing list <a href="mailto:
   109 isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> 
   110 and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to
   111 discuss problems and results.  Why not <a
   112 href="mailto:lcp@cl.cam.ac.uk">subscribe</a>? 
   113