--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/README.html Fri Nov 17 13:22:50 1995 +0100
@@ -0,0 +1,32 @@
+<HTML><HEAD><TITLE>CTT/ReadMe</TITLE></HEAD><BODY>
+
+<H2>CTT: Constructive Type Theory</H2>
+
+This directory contains the Standard ML sources of the Isabelle system for
+Constructive Type Theory (extensional equality, no universes). Important
+files include
+
+<DL>
+<DT>ROOT.ML
+<DD>loads all source files. Enter an ML image containing Pure
+Isabelle and type: use "ROOT.ML";<P>
+
+<DT>Makefile
+<DD>compiles the files under Poly/ML or SML of New Jersey<P>
+
+<DT>ex
+<DD>subdirectory containing examples. To execute them, enter an ML image
+containing CTT and type: use "ex/ROOT.ML";<P>
+</DL>
+
+Useful references on Constructive Type Theory:
+
+<UL>
+<LI> B. Nordström, K. Petersson and J. M. Smith,<BR>
+ Programming in Martin-Löf's Type Theory<BR>
+ (Oxford University Press, 1990)
+
+<LI> Simon Thompson,<BR>
+ Type Theory and Functional Programming (Addison-Wesley, 1991)
+</UL>
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/README.html Fri Nov 17 13:22:50 1995 +0100
@@ -0,0 +1,31 @@
+<HTML><HEAD><TITLE>Cube/ReadMe</TITLE></HEAD><BODY>
+
+<H2>Cube: Barendregt's Lambda-Cube</H2>
+
+This directory contains the Standard ML sources of the Isabelle system for
+the Lambda-Cube. Important files include
+
+<DL>
+<DT>ROOT.ML
+<DD>loads all source files. Enter an ML image containing Pure
+Isabelle and type: use "ROOT.ML";<P>
+
+<DT>Makefile
+<DD>compiles the files under Poly/ML or SML of New Jersey<P>
+
+<DT>ex
+examples file. To execute them, enter an ML image
+containing Cube and type: use "ex.ML";
+</DL>
+
+NB: the formalization is not completely sound! It does not enforce
+distinctness of variable names in contexts!<P>
+
+For more information about the Lambda-Cube, see
+
+<UL>
+<LI>H. Barendregt<BR>
+ Introduction to Generalised Type Systems<BR>
+ J. Functional Programming
+</UL>
+</BODY></HTML>
--- a/src/HOL/README.html Fri Nov 17 13:15:19 1995 +0100
+++ b/src/HOL/README.html Fri Nov 17 13:22:50 1995 +0100
@@ -24,11 +24,12 @@
Useful references on Higher-Order Logic:
<UL>
-<LI>P. B. Andrews, An Introduction to Mathematical Logic and Type Theory
-(Academic Press, 1986).
+<LI>P. B. Andrews,<BR>
+ An Introduction to Mathematical Logic and Type Theory<BR>
+ (Academic Press, 1986).
-<LI>J. Lambek and P. J. Scott, Introduction to Higher Order
-Categorical Logic (CUP, 1986)
+<LI>J. Lambek and P. J. Scott,<BR>
+ Introduction to Higher Order Categorical Logic (CUP, 1986)
</UL>
</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/README.html Fri Nov 17 13:22:50 1995 +0100
@@ -0,0 +1,36 @@
+<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
+
+<H2>HOLCF: A higher order version of LCF based on Isabelle HOL</H2>
+
+Author: Franz Regensburger<BR>
+Copyright 1995 Technische Universität München<P>
+
+Version: 2.0<BR>
+Date: 16.08.95<P>
+
+A detailed description of the entire development can be found in
+
+<UL>
+<LI>Franz Regensburger,<BR>
+ HOLCF: Eine konservative Erweiterung von HOL um LCF,<BR>
+ Dissertation, Technische Universität München, 1994
+</UL>
+
+Changes:
+
+<DL>
+<DT>14.10.94
+<DD>New translation mechanism for continuous infixes
+
+<DT>18.05.95
+<DD>Conversion to curried version of HOL.
+
+<DT>28.06.95
+<DD>The old uncurried version of HOLCF is no longer supported
+ in the distribution.
+
+<DT>18.08.95
+<DD>added sections axioms, ops, domain, genertated
+ and 8bit support
+</DL>
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LCF/README.html Fri Nov 17 13:22:50 1995 +0100
@@ -0,0 +1,27 @@
+<HTML><HEAD><TITLE>LCF/ReadMe</TITLE></HEAD><BODY>
+
+<H2>LCF: Logic for Computable Functions</H2>
+
+This directory contains the Standard ML sources of the Isabelle system for
+LCF. It is loaded upon FOL, not Pure Isabelle. Important files include
+
+<DL>
+<DT>ROOT.ML
+<DD>loads all source files. Enter an ML image containing FOL
+Isabelle and type: use "ROOT.ML";<P>
+
+<DT>Makefile
+<DD>compiles the files under Poly/ML or SML of New Jersey<P>
+
+<DT>ex.ML
+<DD>file containing examples. To execute it, enter an ML image
+containing LCF and type: use "ex.ML";
+</DL>
+
+Useful references on First-Order Logic:
+
+<UL>
+<LI>Lawrence C. Paulson,<BR>
+ Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
+</UL>
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LK/README.html Fri Nov 17 13:22:50 1995 +0100
@@ -0,0 +1,30 @@
+<HTML><HEAD><TITLE>LK/ReadMe</TITLE></HEAD><BODY>
+
+<H2>LK: Classical First-Order Sequent Calculus</H2>
+
+This directory contains the Standard ML sources of the Isabelle system for
+First-Order Logic as a classical sequent calculus. (For a Natural Deduction
+version, see FOL.) Important files include
+
+<DL>
+<DT>ROOT.ML
+<DD>loads all source files. Enter an ML image containing Pure
+Isabelle and type: use "ROOT.ML";<P>
+
+<DT>Makefile
+<DD>compiles the files under Poly/ML or SML of New Jersey<P>
+
+<DT>ex
+<DD>subdirectory containing examples. To execute them, enter an ML image
+containing LK and type: use "ex/ROOT.ML";<P>
+</DL>
+
+Useful references on First-Order Logic:
+
+<UL>
+<LI>Jean Gallier,<BR>
+ Logic for Computer Science (Harper&Row, 1986)
+<LI>G. Takeuti,<BR>
+ Proof Theory (North Holland, 1987)
+</UL>
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Modal/README.html Fri Nov 17 13:22:50 1995 +0100
@@ -0,0 +1,30 @@
+<HTML><HEAD><TITLE>Modal/ReadMe</TITLE></HEAD><BODY>
+
+<H2>Modal: First-Order Modal Sequent Calculus</H2>
+
+This directory contains the Standard ML sources of the Isabelle system for
+Modal Logic. Important files include
+
+<DL>
+<DT>ROOT.ML
+<DD>loads all source files. Enter an ML image containing LK
+Isabelle and type: use "ROOT.ML";<P>
+
+<DT>ex
+<DD>subdirectory containing examples. Files Tthms.ML, S4thms.ML and
+S43thms.ML contain the theorems of Modal Logics, so arranged since
+T<S4<S43. To execute them, enter an ML image containing Modal
+and type: use "ex/ROOT.ML";
+</DL>
+
+Thanks to Rajeev Gore' for supplying the inference system for S43.<P>
+
+Useful references on Modal Logics:
+
+<UL>
+<LI>Melvin C Fitting,<BR>
+ Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
+<LI>Lincoln A. Wallen,<BR>
+ Automated Deduction in Nonclassical Logics (MIT Press, 1990)
+</UL>
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/README.html Fri Nov 17 13:22:50 1995 +0100
@@ -0,0 +1,89 @@
+<HTML><HEAD><TITLE>ZF/ReadMe</TITLE></HEAD><BODY>
+
+<H2>ZF: Zermelo-Fraenkel Set Theory</H2>
+
+This directory contains the Standard ML sources of the Isabelle system for
+ZF Set Theory. It is loaded upon FOL, not Pure Isabelle. Important files
+include
+
+<DL>
+<DT>Makefile
+<DD>compiles the files under Poly/ML or SML of New Jersey. Can also
+run all the tests described below.<P>
+
+<DT>ROOT.ML
+<DD>loads all source files. Enter an ML image containing FOL and
+type: use "ROOT.ML";
+</DL>
+
+There are also several subdirectories of examples. To execute the examples on
+some directory <Dir>, enter an ML image containing ZF and type
+<TT>use "<Dir>/ROOT.ML";</TT>
+
+<DL>
+<DT>AC
+<DD>subdirectory containing proofs from the book "Equivalents of the Axiom
+of Choice, II" by H. Rubin and J.E. Rubin, 1985. Thanks to Krzysztof
+Gr`abczewski.<P>
+
+<DT>Coind
+<DD>subdirectory containing a large example of proof by co-induction. It
+is by Jacob Frost following a paper by Robin Milner and Mads Tofte.<P>
+
+<DT>IMP
+<DD>subdirectory containing a semantics equivalence proof between
+operational and denotational definitions of a simple programming language.
+Thanks to Heiko Loetzbeyer & Robert Sandner.<P>
+
+<DT>Resid
+<DD>subdirectory containing a proof of the Church-Rosser Theorem. It is
+by Ole Rasmussen, following the Coq proof by Gérard Huet.<P>
+
+<DT>ex
+<DD>subdirectory containing various examples.
+</DL>
+
+Isabelle/ZF formalizes the greater part of elementary set theory,
+including relations, functions, injections, surjections, ordinals and
+cardinals. Results proved include Cantor's Theorem, the Recursion
+Theorem, the Schroeder-Bernstein Theorem, and (assuming AC) the
+Wellordering Theorem.<P>
+
+Isabelle/ZF also provides theories of lists, trees, etc., for
+formalizing computational notions. It supports inductive definitions
+of infinite-branching trees for any cardinality of branching.<P>
+
+Useful references for Isabelle/ZF:
+
+<UL>
+<LI> Lawrence C. Paulson,<BR>
+ Set theory for verification: I. From foundations to functions.<BR>
+ J. Automated Reasoning 11 (1993), 353-389.
+
+<LI> Lawrence C. Paulson,<BR>
+ Set theory for verification: II. Induction and recursion.<BR>
+ Report 312, Computer Lab (1993).<BR>
+
+<LI> Lawrence C. Paulson,<BR>
+ A fixedpoint approach to implementing (co)inductive definitions. <BR>
+ In: A. Bundy (editor),<BR>
+ CADE-12: 12th International Conference on Automated Deduction,<BR>
+ (Springer LNAI 814, 1994), 148-161.
+</UL>
+
+Useful references on ZF set theory:
+
+<UL>
+<LI> Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
+
+<LI> Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
+
+<LI> Keith J. Devlin,<BR>
+ Fundamentals of Contemporary Set Theory (Springer, 1979)
+
+<LI> Kenneth Kunen<BR>
+ Set Theory: An Introduction to Independence Proofs<BR>
+ (North-Holland, 1980)
+</UL>
+
+</BODY></HTML>