--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/index.html	Mon Nov 02 21:15:55 1998 +0100
@@ -0,0 +1,139 @@
+
+<html>
+
+<head>
+<title>Isabelle</title>
+
+<body>
+
+<h1>Isabelle </h1> <a href="http://www.in.tum.de/~isabelle/logo/"><img
+src="isabelle.gif" width=100 align=right alt="[Isabelle logo]"></a>
+
+<p>
+
+<strong>Isabelle</strong> 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>).
+The latest version is <strong>Isabelle98-1</strong>. It is available
+from several <a href="dist/">mirror sites</a>.
+
+<p>
+
+Isabelle can be viewed from two main perspectives.  On the one hand it
+may serve as a generic framework for rapid prototyping of deductive
+systems.  On the other hand, major object logics, like
+<strong>Isabelle/HOL</strong>, provide a theorem proving environment
+ready to use for sizable applications.
+
+
+<h2>Object logics</h2>
+
+The Isabelle distribution includes o large body of object logics and
+other examples (see the <a
+href="http://www.in.tum.de/~isabelle/library/">Isabelle theory
+library</a>.
+
+<dl>
+
+<dt><a
+href="http://www.in.tum.de/~isabelle/library/HOL/"><strong>Isabelle/HOL</strong></a><dd>
+is a version of classical higher-order logic, similar to Gordon's HOL
+(it is related to Church's Simple Theory of Types).
+
+<dt><a
+href="http://www.in.tum.de/~isabelle/library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd>
+adds a considerably amount of Scott's domain theory to HOL.
+
+<dt><a
+href="http://www.in.tum.de/~isabelle/library/FOL/"><strong>Isabelle/FOL</strong></a><dd>
+provides basic classical and intuitionistic first-order (polymorphic)
+logic.
+
+<dt><a
+href="http://www.in.tum.de/~isabelle/library/ZF/"><strong>Isabelle/ZF</strong></a><dd>
+offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
+
+</dl>
+
+<p>
+
+Isabelle/HOL is currently the best developed object logic, including
+an extensive library of (concrete) mathematics, and various packages
+for advanced definitional concepts (like (co-)inductive sets and
+types, well-founded recursion etc.).  The distribution also includes
+some large applications, for example correctness proofs of
+cryptographic protocols (<a
+href="http://www.in.tum.de/~isabelle/library/HOL/Auth/">HOL/Auth</a>).
+
+<p>
+
+Isabelle/ZF provides another starting point for applications, with a
+slightly less developed library, though.  Its definitional packages
+are similar to those of Isabelle/HOL.  Untyped ZF provides more
+advanced constructions for sets than simply typed HOL.
+
+<p>
+
+There are also a few minor object logics that may serve as further
+examples: <a
+href="http://www.in.tum.de/~isabelle/library/CTT/">CTT</a> is an
+extensional version of Martin-L&ouml;f's Type Theory, <a
+href="http://www.in.tum.de/~isabelle/library/Cube/">Cube</a> is
+Barendregt's Lambda Cube.  There are also some sequent calculus
+examples under <a
+href="http://www.in.tum.de/~isabelle/library/Sequents/">Sequents</a>,
+including modal or linear logics.  There are a few more examples,
+again see the <a
+href="http://www.in.tum.de/~isabelle/library/">Isabelle theory
+library</a>.
+
+
+<h2>Defining Logics</h2>
+
+Logics are not hard-wired into Isabelle, but formulated within
+Isabelle's meta logic: <strong>Isabelle/Pure</strong>.  There are
+quite a lot of syntactic and deductive tools available.  Thus defining
+new logics or extending existing ones basically works as follows:
+
+<ol>
+
+<li> declare concrete syntax (via mixfix grammar and syntax macros),
+
+<li> declare abstract syntax (as higher-order constants),
+
+<li> declare inference rules (as meta-logical propositions),
+
+<li> instantiate generic proof tools (simplifier, classical tableau
+prover etc.),
+
+<li> manually code special proof procedures (via tacticals or hand
+written ML).
+
+</ol>
+
+The first 3 steps are fully declarative and involve no ML programming
+at all.  Thus one already gets a decent deductive environment based on
+primitive inferences (by employing the built-in mechanisms of
+Isabelle/Pure, in particular higher-order unification and resolution).
+
+For sizable applications some degree of automated reasoning is
+essential.  Instantiating existing tools like the classical tableau
+prover involves only minimal ML based setup.  One may also write
+arbitrary proof procedures or even theory extension packages in ML,
+without breaching system soundness (Isabelle follows the well-known
+"LCF system approach").
+
+
+<h2>Further information</h2>
+
+<a href="http://www.cl.cam.ac.uk/Research/HVG/isabelle.html"><img
+src="cambridge.gif" width=144 align=right alt="[Cambridge]"></a> <a
+href="http://www.in.tum.de/~isabelle/"><img src="munich.gif" width=47
+align=right alt="[Munich]"></a> The local Isabelle pages at <a
+href="http://www.cl.cam.ac.uk/Research/HVG/isabelle.html">Cambridge</a>
+and <a href="http://www.in.tum.de/~isabelle/">Munich</a> provide
+further information on Isabelle and related projects.
+
+
+</html>