author kleing
Mon, 19 Apr 2004 08:20:52 +0200
changeset 14624 9b3397a848c3
parent 14615 603f08285c65
child 14637 d258f6c11d83
permissions -rw-r--r--
add HOL4




<h2>What is Isabelle?</h2>

Isabelle is a popular generic theorem proving environment developed at
Cambridge University (<a
href="">Larry Paulson</a>) and TU
Munich (<a href="">Tobias Nipkow</a>).
See the <a href="overview.html">Isabelle overview</a>.


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


at Cambridge</strong></a>

<li><a href=""><strong>Isabelle
at Munich</strong></a>


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


<h2><!-- _GP_ distname --></h2>
New features in <strong><!-- _GP_ distname --></strong> include
<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>Presentation and x-symbol enhancements, greek letters and
sub/superscripts allowed in identifiers.</li>
<a href="dist/<!-- _GP_ distname -->/NEWS">[Complete Changelog]</a>
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. There is also
a nightly generated <a href="">development 
snapshot</a> available.


<h2>Out now</h2>

<a href="dist/<!-- _GP_ distname -->/doc/tutorial.pdf">Tutorial on Isabelle/HOL</a> --
published by Springer Verlag as <a
href="">LNCS 2283</a>.


You can also browse the <a href="library/index.html">Isabelle theory
library</a>; the main logics are <a
href="library/HOL/index.html">HOL</a>, <a
href="library/HOLCF/index.html">HOLCF</a>, <a
href="library/FOL/index.html">FOL</a> and <a


<h2>Mailing list</h2>

Use the mailing list <a href="mailto:"></a> 
and its <a href="">archive</a> to
discuss problems and results.  Why not <a