--- a/src/Cube/README Wed Oct 09 13:38:11 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
- Cube: Barendregt's Lambda-Cube
-
-This directory contains the Standard ML sources of the Isabelle system for
-the Lambda-Cube. Important files include
-
-ROOT.ML -- loads all source files. Enter an ML image containing Pure
-Isabelle and type: use "ROOT.ML";
-
-Makefile -- compiles the files under Poly/ML or SML of New Jersey
-
-ex.ML -- examples file. To execute them, enter an ML image
-containing Cube and type: use "ex.ML";
-
-NB: the formalization is not completely sound! It does not enforce
-distinctness of variable names in contexts!
-
-For more information about the Lambda-Cube, see
- H. Barendregt
- Introduction to Generalised Type Systems
- J. Functional Programming
-
--- a/src/FOL/README Wed Oct 09 13:38:11 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
- FOL: First-Order Logic with Natural Deduction
-
-This directory contains the Standard ML sources of the Isabelle system for
-First-Order Logic (constructive and classical versions). For a classical
-sequent calculus, see LK. Important files include
-
-ROOT.ML -- loads all source files. Enter an ML image containing Pure
-Isabelle and type: use "ROOT.ML";
-
-Makefile -- compiles the files under Poly/ML or SML of New Jersey
-
-ex -- subdirectory containing examples. To execute them, enter an ML image
-containing FOL and type: use "ex/ROOT.ML";
-
-Useful references on First-Order Logic:
-
- Antony Galton, Logic for Information Technology (Wiley, 1990)
-
- Michael Dummett, Elements of Intuitionism (Oxford, 1977)
\ No newline at end of file
--- a/src/HOL/README Wed Oct 09 13:38:11 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
- HOL: Higher-Order Logic with curried functions
-
-This directory contains the Standard ML sources of the Isabelle system for
-Higher-Order Logic with curried functions. Important files include
-
-ROOT.ML -- loads all source files. Enter an ML image containing Pure
-Isabelle and type: use "ROOT.ML";
-
-Makefile -- compiles the files under Poly/ML or SML of New Jersey
-
-ex -- subdirectory containing examples. To execute them, enter an ML image
-containing HOL and type: use "ex/ROOT.ML";
-
-Subst -- subdirectory defining a theory of substitution and unification.
-
-Useful references on Higher-Order Logic:
-
- P. B. Andrews,
- An Introduction to Mathematical Logic and Type Theory
- (Academic Press, 1986).
-
- J. Lambek and P. J. Scott,
- Introduction to Higher Order Categorical Logic (CUP, 1986)
--- a/src/HOLCF/README Wed Oct 09 13:38:11 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-HOLCF: A higher order version of LCF based on Isabelle HOL
-==========================================================
-
-Author: Franz Regensburger
-Copyright 1995 Technische Universitaet Muenchen
-
-Version: 2.0
-Date: 16.08.95
-
-A detailed description of the entire development can be found in
-
-[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
- Dissertation, Technische Universit"at M"unchen, 1994
-
-Changes:
-14.10.94 New translation mechanism for continuous infixes
-18.05.95 Conversion to curried version of HOL.
-
-28.06.95 The old uncurried version of HOLCF is no longer supported
- in the distribution.
-
-18.08.95 added sections axioms, ops, domain, generated
- and optional 8bit support
-
--- a/src/LCF/README Wed Oct 09 13:38:11 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
- LCF: Logic for Computable Functions
-
-This directory contains the Standard ML sources of the Isabelle system for
-LCF. It is loaded upon FOL, not Pure Isabelle. Important files include
-
-ROOT.ML -- loads all source files. Enter an ML image containing FOL and
-type: use "ROOT.ML";
-
-Makefile -- compiles the files under Poly/ML or SML of New Jersey
-
-ex.ML -- files containing examples. To execute them, enter an ML image
-containing LCF and type: use "ex.ML";
-
-Useful references on LCF:
-
- Lawrence C. Paulson,
- Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
-
--- a/src/LK/README Wed Oct 09 13:38:11 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
- LK: Classical First-Order Sequent Calculus
-
-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
-
-ROOT.ML -- loads all source files. Enter an ML image containing Pure
-Isabelle and type: use "ROOT.ML";
-
-Makefile -- compiles the files under Poly/ML or SML of New Jersey
-
-ex -- subdirectory containing examples. To execute them, enter an ML image
-containing LK and type: use "ex/ROOT.ML";
-
-
-Useful references on sequent calculi:
-
- Jean Gallier, Logic for Computer Science (Harper&Row, 1986)
-
- G. Takeuti, Proof Theory (North Holland, 1987)
--- a/src/Modal/README Wed Oct 09 13:38:11 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
- Modal: First-Order Modal Sequent Calculus
-
-This directory contains the Standard ML sources of the Isabelle system for
-Modal Logic. Important files include
-
-ROOT.ML -- loads all source files. Enter an ML image containing LK
- and type: use "ROOT.ML";
-
-ex -- 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";
-
-Thanks to Rajeev Gore' for supplying the inference system for S43.
-
-Useful references on Modal Logics:
-
- Melvin C Fitting,
- Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
-
- Lincoln A. Wallen,
- Automated Deduction in Nonclassical Logics (MIT Press, 1990)
--- a/src/ZF/README Wed Oct 09 13:38:11 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
- ZF: Zermelo-Fraenkel Set Theory
-
-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
-
-Makefile -- compiles the files under Poly/ML or SML of New Jersey. Can also
-run all the tests described below.
-
-ROOT.ML -- loads all source files. Enter an ML image containing FOL and
-type: use "ROOT.ML";
-
-There are also several subdirectories of examples. To execute the examples on
-some directory <Dir>, enter an ML image containing ZF and type
- use "<Dir>/ROOT.ML";
-
-AC -- 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.
-
-Coind -- subdirectory containing a large example of proof by co-induction. It
-is by Jacob Frost following a paper by Robin Milner and Mads Tofte.
-
-IMP -- subdirectory containing a semantics equivalence proof between
-operational and denotational definitions of a simple programming language.
-Thanks to Heiko Loetzbeyer & Robert Sandner.
-
-Resid -- subdirectory containing a proof of the Church-Rosser Theorem. It is
-by Ole Rasmussen, following the Coq proof by Gérard Huet.
-
-ex -- subdirectory containing various examples.
-
-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.
-
-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.
-
-Useful references for Isabelle/ZF:
-
- Lawrence C. Paulson,
- Set theory for verification: I. From foundations to functions.
- J. Automated Reasoning 11 (1993), 353-389.
-
- Lawrence C. Paulson,
- Set theory for verification: II. Induction and recursion.
- Report 312, Computer Lab (1993).
-
- Lawrence C. Paulson,
- A fixedpoint approach to implementing (co)inductive definitions.
- In: A. Bundy (editor),
- CADE-12: 12th International Conference on Automated Deduction,
- (Springer LNAI 814, 1994), 148-161.
-
-Useful references on ZF set theory:
-
- Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
-
- Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
-
- Keith J. Devlin,
- Fundamentals of Contemporary Set Theory (Springer, 1979)
-
- Kenneth Kunen
- Set Theory: An Introduction to Independence Proofs
- (North-Holland, 1980)
-
-$Id$