Admin/website/index.html
changeset 16233 e634d33deb86
child 16240 95cc0e8f8a17
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/index.html	Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,124 @@
+<?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">
+<?cvs id="$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>
+        These pages provide general information on Isabelle, more
+        specific information is available from the local pages
+        </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>Coming soon: Isabelle 2005</h2>
+         <p>New features in the upcoming Isabelle 2005 will include</p>
+              <ul>
+                <li>New commands for instantiating locales</li>
+                <li>New command for finding matching rewrite rules</li>
+                <li>Finding theorems by term patterns</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>
+                <li>New syntax that will allow &gt; and &gt;= in addition to &lt; and
+                &lt;=</li>
+              </ul>
+
+        <h2>Isabelle 2004</h2> 
+
+<p>New features in Isabelle 2004 include</p>
+
+<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>
+
+<p><a href="isabelle/Isabelle/NEWS">[Complete Changelog]</a></p>
+
+<h2>Download</h2>
+
+<p>
+The Isabelle 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. 
+</p>
+
+<p>
+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&amp;body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">contact Larry Paulson</a>.
+</p>
+
+    </div>
+    <div class="hr"><hr/></div>
+    <?include file="//include/footer.include.html"?>
+</body>
+
+</html>