Admin/page/index.html

 
 <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>
+<a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><img
+src="cambridge.gif" width=145 border=0 align=right
+alt="[Cambridge]"></a> <a
+href="http://www.in.tum.de/~isabelle/munich.html"><img
+src="munich.gif" width=48 border=0 align=right alt="[Munich]"></a> 
 
+This page provides general information on Isabelle, more details are 
+available on the local Isabelle pages  at 
+ <a
+href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">Cambridge</a>
+and <a href="http://www.in.tum.de/~isabelle/munich.html">Munich</a>. 
+See there for informations on projects done with Isabelle, mailing list archives, 
+research papers, the Isabelle bibliography, and Isabelle workshops and courses. 
+
+
+
+<h2>Obtaining Isabelle</h2>
+The latest version is <strong>Isabelle98-1</strong>, it is available
+from several mirror sites (given in alphabetical order):
+
+<ul>
+
+<li> <a
+href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/">Cambridge
+(UK)</a>
+
+<li> <a
+href="ftp://ftp.ci.uminho.pt/pub/mirrors/isabelle/index.html">Minho
+(Portugal)</a>
+
+<li> <a
+href="http://www4.informatik.tu-muenchen.de/~isabelle/dist/">Munich
+(Germany)</a>
+
+<li> <a
+href="ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html">New
+Jersey (USA)</a>
+
+</ul>
+<p>
+
+
+<h2>What is  Isabelle?</h2>
 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
+systems.  On the other hand, major existing logics like
 <strong>Isabelle/HOL</strong> provide a theorem proving environment
 ready to use for sizable applications.
 
 
-<h2>Object logics</h2>
+<h3>Isabelle's Logics</h3>
 
 The Isabelle distribution includes a large body of object logics and
 other examples (see the <a href="library/">Isabelle theory
 library</a>).
 

 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="library/HOL/Auth/">HOL/Auth</a>).
+href="library/HOL/Auth/">HOL/Auth</a>) or communication protocols (<a
+href="library/HOLCF/IOA/">HOLCF/IOA</a>).
 
 <p>
 
 Isabelle/ZF provides another starting point for applications, with a
 slightly less developed library.  Its definitional packages

 including modal and linear logics.  Again see the <a
 href="library/">Isabelle theory
 library</a> for other examples.
 
 
-<h2>Defining Logics</h2>
+<h3>Defining Logics</h3>
 
 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 in generic
 Isabelle.  Thus defining new logics or extending existing ones

 arbitrary proof procedures or even theory extension packages in ML,
 without breaching system soundness (Isabelle follows the well-known
 <em>LCF system approach</em> to achieve a secure system).
 
 
-<H2>Mailing list</H2>
-
-<P>Use the mailing list 
-<A HREF="mailto: [e-mail]">[e-mail]</A> 
-to discuss problems and results.  
 
 <h2>Further information</h2>
-
-<a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><img
-src="cambridge.gif" width=145 border=0 align=right
-alt="[Cambridge]"></a> <a
-href="http://www.in.tum.de/~isabelle/munich.html"><img
-src="munich.gif" width=48 border=0 align=right alt="[Munich]"></a> The
-cambridge Isabelle pages at <a
+See the local Isabelle pages  at 
+ <a
 href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html">Cambridge</a>
-and <a href="http://www.in.tum.de/~isabelle/munich.html">Munich</a>
-provide further information on Isabelle and related projects.
-
+and <a href="http://www.in.tum.de/~isabelle/munich.html">Munich</a>. 
 </body>
 
 </html>