summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

Admin/page/index.html

changeset 5806 | 9d30b79832e8 |

parent 5805 | e867bc95a47d |

child 5807 | bd2d9dd34dfd |

--- a/Admin/page/index.html Fri Nov 06 13:42:13 1998 +0100 +++ b/Admin/page/index.html Fri Nov 06 13:58:59 1998 +0100 @@ -34,15 +34,14 @@ Isabelle workshops and courses. +<h2>Obtaining Isabelle</h2> -<h2>Obtaining Isabelle</h2> The latest version is <strong>Isabelle98-1</strong>, it is available -from several -<a href="dist/">mirror sites</a>. - +from several <a href="dist/">mirror sites</a>. <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 existing logics like @@ -58,19 +57,20 @@ <dl> -<dt><a href="library/HOL/"><strong>Isabelle/HOL</strong></a><dd> -is a version of classical higher-order logic resembling that of the -<A HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL System</A>. +<dt><a href="library/HOL/"><strong>Isabelle/HOL</strong></a><dd> is a +version of classical higher-order logic resembling that of the <A +HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL +System</A>. <dt><a href="library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd> adds Scott's Logic for Computable Functions (domain theory) to HOL. <dt><a href="library/FOL/"><strong>Isabelle/FOL</strong></a><dd> -provides basic classical and intuitionistic first-order logic. -It is polymorphic. +provides basic classical and intuitionistic first-order logic. It is +polymorphic. -<dt><a href="library/ZF/"><strong>Isabelle/ZF</strong></a><dd> -offers a formulation of Zermelo-Fraenkel set theory on top of FOL. +<dt><a href="library/ZF/"><strong>Isabelle/ZF</strong></a><dd> offers +a formulation of Zermelo-Fraenkel set theory on top of FOL. </dl> @@ -81,30 +81,25 @@ 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>) or communication protocols (<a -href="library/HOLCF/IOA/">HOLCF/IOA</a>). +cryptographic protocols (<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 -are similar to those of Isabelle/HOL. Untyped ZF provides more -advanced constructions for sets than simply-typed HOL. +slightly less developed library. 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 a few minor object logics that may serve as further -examples: <a -href="library/CTT/">CTT</a> is an -extensional version of Martin-Löf's Type Theory, <a -href="library/Cube/">Cube</a> is +examples: <a href="library/CTT/">CTT</a> is an extensional version of +Martin-Löf's Type Theory, <a href="library/Cube/">Cube</a> is Barendregt's Lambda Cube. There are also some sequent calculus -examples under <a -href="library/Sequents/">Sequents</a>, -including modal and linear logics. Again see the <a -href="library/">Isabelle theory -library</a> for other examples. +examples under <a href="library/Sequents/">Sequents</a>, including +modal and linear logics. Again see the <a href="library/">Isabelle +theory library</a> for other examples. <h3>Defining Logics</h3> @@ -144,12 +139,12 @@ 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: isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</A> - to discuss problems and results. + +<h2>Mailing list</h2> +Use the mailing list <a href="mailto: +isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to +discuss problems and results. </body>