author wenzelm
Tue, 27 Sep 2005 17:24:27 +0200
changeset 17684 c98508731bd6
parent 17671 e9e341bc7d42
child 17692 6d277e731096
permissions -rw-r--r--
more details about incomplete 'defs';

<?xml version='1.0' encoding='iso-8859-1' ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "">
<!-- $Id$ -->
<html xmlns="">

    <?include file="//include/htmlheader.include.html"?>

<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> 
        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
        This site provides general information on Isabelle, more
        specific information is available from the local sites


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

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


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

        <h2>Now available: Isabelle 2005</h2>
         <p>Some notable features:</p>
	      <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>
              <li>More well-formedness checks of overloaded
                  definitions, but fails to recognize certain ill-formed definitions
                  that Isabelle2004 would have rejected outright!</li>

<p><a href="//dist/Isabelle/NEWS">[Cumulative NEWS]</a></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.

Use the mailing list <a href=
          ""></a> and its
          <a href="">archive</a> to
discuss problems and results.  To subscribe, <a href=
          contact our robot</a>.

    <div class="hr"><hr/></div>
    <?include file="//include/footer.include.html"?>