summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 03 Nov 1998 09:47:49 +0100 | |

changeset 5798 | cc32a1c16710 |

parent 5797 | cdd2add0fd96 |

child 5799 | 8419bd5f85fc |

tuned;

--- a/Admin/page/index.html Mon Nov 02 22:18:35 1998 +0100 +++ b/Admin/page/index.html Tue Nov 03 09:47:49 1998 +0100 @@ -16,7 +16,7 @@ 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 +The latest version is <strong>Isabelle98-1</strong>, it is available from several <a href="dist/">mirror sites</a>. <p> @@ -48,8 +48,8 @@ <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. +provides basic classical and intuitionistic first-order logic +(polymorphic). <dt><a href="http://www.in.tum.de/~isabelle/library/ZF/"><strong>Isabelle/ZF</strong></a><dd> @@ -72,11 +72,11 @@ 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. +advanced constructions for sets than simply-typed HOL. <p> -There are also a few minor object logics that may serve as further +There are 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öf's Type Theory, <a @@ -84,7 +84,7 @@ 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. Again see the <a +including modal and linear logics. Again see the <a href="http://www.in.tum.de/~isabelle/library/">Isabelle theory library</a> for other examples. @@ -113,7 +113,7 @@ </ol> -The first 3 steps above are fully declarative and involve no ML +The first three steps above 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