--- a/Admin/page/main-content/index.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-%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 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 > and >= in addition to < and <=</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="mailto:isabelle-lemmas@cl.cam.ac.uk">isabelle-lemmas@cl.cam.ac.uk</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="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</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="mailto:lcp@cl.cam.ac.uk?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">contact Larry Paulson</a>.
-