Simplified version of Jia's filter. Now all constants are pooled, rather than
relevance being compared against separate clauses. Rejects are no longer noted,
and units cannot be added at the end.
<?xml version='1.0' encoding='iso-8859-1' ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<!-- $Id$ -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Isabelle</title>
<?include file="//include/htmlheader.include.html"?>
</head>
<body class="main">
<?include file="//include/header.include.html"?>
<div class="hr"><hr/></div>
<?include file="//include/navigation.include.html"?>
<div class="hr"><hr/></div>
<div id="content">
<h2>What is Isabelle?</h2>
<p>
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>
<p>
This site provides general information on Isabelle, more
specific information is available from the local sites
</p>
<ul>
<li><a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
at Cambridge</strong></a></li>
<li><a href="http://www4.in.tum.de/proj/theoremprov/group.html"><strong>Isabelle
at Munich</strong></a></li>
</ul>
<p>
See there for information on projects done with Isabelle,
mailing list archives, research papers, the Isabelle
bibliography, and Isabelle workshops and courses.
</p>
<h2>Now available: Isabelle2005</h2>
<p>Some highlights:</p>
<ul>
<li>Interpretation of locale expressions in theories, locales, and proof contexts.</li>
<li>Substantial library improvements (HOL, HOL-Complex, HOLCF).</li>
<li>Proof tools for transitivity reasoning.</li>
<li>General <code>find_theorems</code> command (by term patterns, as intro/elim/simp rules etc.).</li>
<li>Commands for generating adhoc draft documents.</li>
<li>Support for Unicode proof documents (UTF-8).</li>
<li>Major internal reorganizations and performance improvements.</li>
</ul>
<p><a href="//dist/Isabelle/NEWS">[Cumulative NEWS]</a></p>
<h2>Download</h2>
<p>
Isabelle is distributed for free under the BSD license. It includes
source and binary packages and browsable documentation, see the <a
href="installation.html">installation instructions</a>. You can also
browse the <a href="//dist/library/index.html">Isabelle theory
library</a> online.
</p>
<p>
Use the mailing list <a href=
"mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> and its
<a href="https://lists.cam.ac.uk/pipermail/cl-isabelle-users/index.html">archive</a> to
discuss problems and results. To subscribe, <a href=
"mailto:Cl-isabelle-users-request@lists.cam.ac.uk?subject=subscribe">
contact our robot</a>.
</p>
</div>
<div class="hr"><hr/></div>
<?include file="//include/footer.include.html"?>
</body>
</html>