Admin/page/main-content/index.content

obscured the e-mail address lcp@cl

%title%
Isabelle

%body%

<p>

<h2>What is Isabelle?</h2>

Isabelle is a popular generic theorem proving environment developed at
Cambridge University (<a
href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
See the <a href="overview.html">Isabelle overview</a>.

<p>

These pages provide general information on Isabelle, more specific
information is available from the local pages

<ul>

<li><a
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
at Cambridge</strong></a>

<li><a href="http://www4.in.tum.de/proj/theoremprov/group.html"><strong>Isabelle
at Munich</strong></a>

</ul>

See there for information on projects done with Isabelle, mailing list
archives, research papers, the Isabelle bibliography, and Isabelle
workshops and courses.

<p>

<h2>Isabelle 2005 - Preview</h2>

<ul>
<li>New command for finding matching rewrite rules</li>
<li>New syntax to allow &gt; and &gt;=</li>
<li>New automatic transitivity reasoner</li>
<li>New command for ad-hoc theory viewing and printing</li>
<li>Much extended and improved theory of finite sets</li>
</ul>

<h2>Contributing</h2> 

Did you have to prove a lemma that should have been part of the
Isabelle distribution?  Send it to us!  <p> We will collect theorems
sent to <a
href="&#109;&#97;&#105;&#108;&#116;&#111;:&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#108;&#101;&#109;&#109;&#97;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;">&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#108;&#101;&#109;&#109;&#97;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;</a>.
Accepted material will be included in the Isabelle sources, with
credit given to the author. Note that the Isabelle sources are
distributed under the BSD license.  Lemmas should be general, useful,
and not too large. For larger developments you might want to consider
a submission to the <a href="http://afp.sf.net">Archive of Formal
Proofs</a>.


<h2>Course Material, Exercises</h2>

The <a
href="http://isabelle.in.tum.de/coursematerial/">course material</a>
page makes slides, demos, and exercises of a growing number of
Isabelle courses available. It is meant as a resource for people 
who would like to learn Isabelle as well as for those who would like 
to teach it.

<p>

<h2>AFP - The Archive of Formal Proofs</h2>

The <a href="http://afp.sf.net">Archive of Formal Proofs</a> is a
collection of proof libraries, examples, and larger scientifc
developments, mechanically checked in Isabelle. It is organized in the
way of a scientific journal. Submissions are refereed.

<p>

<h2><!-- _GP_ distname --></h2>
New features in <strong><!-- _GP_ distname --></strong> include
<ul>
<li>New image HOL4 with imported library from HOL4 system on top of
  HOL-Complex (about 2500 additional theorems).</li>

<li>New theory Ring_and_Field with over 250 basic numerical laws, 
  all proved in axiomatic type classes for semirings, rings and fields.</li>

<li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li>

<li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>

<li>New theory of matrices with an application to linear programming in HOL-Matrix.</li>

<li>Improved locales (named proof contexts), instantiation of locales.</li>

<li>Improved handling of linear and partial orders in simplifier.</li>
 
<li>New <code>specification</code> command for definition by specification.</li>  

<li>New Isar command <code>finalconsts</code> prevents constants being given a definition later.</li>  

<li><code>arith</code> now generates counterexamples for reals as well.</li>

<li>New <code>quickcheck</code> command
    to search for counterexamples of executable goals.
  (see HOL/ex/Quickcheck_Examples.thy)</li>
<li>New <code>refute</code> command
    to search for finite countermodels of goals.
  (see HOL/ex/Refute_Examples.thy)
</li>

<li>Presentation and x-symbol enhancements, greek letters and
sub/superscripts allowed in identifiers.</li>
</ul>
<a href="dist/<!-- _GP_ distname -->/NEWS">[Complete Changelog]</a>
<p>
The <strong><!-- _GP_ distname --></strong> distribution is available
from several <a href="dist/index.html">mirror sites</a>.  It includes
source and binary packages and browsable documentation. You can also
browse the <a href="library/index.html">Isabelle theory library</a>
online. For the curious, there is a nightly generated <a
href="http://isabelle.in.tum.de/devel/">development snapshot</a>
available.

<p>

<h2>Mailing list</h2>

Use the mailing list <a
href="&#109;&#97;&#105;&#108;&#116;&#111;:&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#117;&#115;&#101;&#114;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;">&#105;&#115;&#97;&#98;&#101;&#108;&#108;&#101;-&#117;&#115;&#101;&#114;&#115;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;</a>
and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to
discuss problems and results.  To subscribe, <a href="&#109;&#97;&#105;&#108;&#116;&#111;:&#108;&#99;&#112;&#64;&#99;&#108;&#46;&#99;&#97;&#109;&#46;&#97;&#99;&#46;&#117;&#107;?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">contact Larry Paulson</a>.