# HG changeset patch # User wenzelm # Date 864227580 -7200 # Node ID 815ef58483246fa8f5337845102b652f50836724 # Parent 636322bfd05798a3b047aa0aa55311336a918cdc tuned all READMEs; diff -r 636322bfd057 -r 815ef5848324 README.html --- a/README.html Wed May 21 17:11:46 1997 +0200 +++ b/README.html Wed May 21 17:13:00 1997 +0200 @@ -32,7 +32,7 @@ distribution:

A full Standard ML Compiler (e.g. Poly/ML or SML of New Jersey). -
The GNU bash shell (version 1.14.x or 2.x). +
The GNU bash shell (version 1.x or 2.x).
Perl 5.x - the Pathologically Eclectic Rubbish Lister.

@@ -44,8 +44,7 @@ The following ML system and platform combinations are known to work quite well:

Poly/ML versions 2.x and 3.1 on Suns (running SunOS 4.1.x or -Solaris 2.x). +
Poly/ML versions 2.x and 3.1 on Suns.
SML/NJ 0.93 on Suns and SGIs. There seem to be several problems with Linux and HP-UX.
SML/NJ 1.07 on Suns, Linux, etc. diff -r 636322bfd057 -r 815ef5848324 src/CTT/README.html --- a/src/CTT/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/CTT/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,23 +1,12 @@ -CTT/ReadMe + +CTT/README
CTT: Constructive Type Theory
-This directory contains the Standard ML sources of the Isabelle system for -Constructive Type Theory (extensional equality, no universes). Important -files include +This directory contains the ML sources of the Isabelle system for +Constructive Type Theory (extensional equality, no universes).
-
-
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 CTT and type: use "ex/ROOT.ML";
-
+The ex subdirectory contains some examples.
Useful references on Constructive Type Theory: @@ -29,4 +18,6 @@
Simon Thompson,
Type Theory and Functional Programming (Addison-Wesley, 1991)

- + + + diff -r 636322bfd057 -r 815ef5848324 src/Cube/README.html --- a/src/Cube/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/Cube/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,22 +1,12 @@ -Cube/ReadMe + +Cube/README

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";

+This directory contains the ML sources of the Isabelle system for the +Lambda-Cube.

Makefile -

compiles the files under Poly/ML or SML of New Jersey

- -

ex -examples file. To execute them, enter an ML image -containing Cube and type: use "ex.ML"; -

+The ex subdirectory contains some examples.

NB: the formalization is not completely sound! It does not enforce distinctness of variable names in contexts!

@@ -28,4 +18,5 @@ Introduction to Generalised Type Systems
J. Functional Programming - + + diff -r 636322bfd057 -r 815ef5848324 src/FOL/README.html --- a/src/FOL/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/FOL/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,27 +1,19 @@ -FOL/ReadMe +FOL/README

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 +This directory contains the ML sources of the Isabelle system for +First-Order Logic (constructive and classical versions). For a +classical sequent calculus, see LK.

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";
-

+The ex subdirectory contains some examples.

Useful references on First-Order Logic:

Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 1991)
+ (The first chapter is an excellent introduction to natural +deduction in general.)
Antony Galton, Logic for Information Technology (Wiley, 1990)
Michael Dummett, Elements of Intuitionism (Oxford, 1977)

diff -r 636322bfd057 -r 815ef5848324 src/HOL/AxClasses/README.html --- a/src/HOL/AxClasses/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/HOL/AxClasses/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,4 +1,6 @@ -HOL/AxClasses/ReadMe +HOL/AxClasses/README + +

Axiomatic type classes

This directory contains the following axiomatic type class examples: diff -r 636322bfd057 -r 815ef5848324 src/HOL/IOA/README.html --- a/src/HOL/IOA/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/HOL/IOA/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,4 +1,4 @@ -HOLCF/ReadMe +HOLCF/IOA/README

IOA: A basic formalization of I/O automata in HOL

diff -r 636322bfd057 -r 815ef5848324 src/HOL/Lex/README.html --- a/src/HOL/Lex/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/HOL/Lex/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,4 +1,4 @@ -HOL/Lex/ReadMe +HOL/Lex/README

A Simplified Scanner Generator

@@ -34,15 +34,5 @@ diagram, i.e. the translation of regular expressions into deterministic finite automata is still missing.

M.Sc./Diplom/Fopra Project

- -Task: formalize the translation of regular expressions into deterministic -finite automata. We are looking for a theoretically inclined student who -likes automata theory and is not afraid of logic and proofs. Sounds -interesting? Then contact Tobias Nipkow or Cornelia Pusch. -This project is also suitable as a joint "Fopra" for two students. - diff -r 636322bfd057 -r 815ef5848324 src/HOL/Modelcheck/README.html --- a/src/HOL/Modelcheck/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/HOL/Modelcheck/README.html Wed May 21 17:13:00 1997 +0200 @@ -2,7 +2,7 @@

Invoking Model Checkers in Isabelle/HOL

-Authors: Olaf Mueller, Jan Philipps, Robert Sandner
+Authors: Olaf Müller, Jan Philipps, Robert Sandner
Copyright 1997 Technische Universität München

diff -r 636322bfd057 -r 815ef5848324 src/HOL/README.html --- a/src/HOL/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/HOL/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,26 +1,12 @@ -HOL/ReadMe +HOL/README -

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 +

HOL: Higher-Order Logic

ROOT.ML -

loads all source files. Enter an ML image containing Pure -Isabelle and type: use "ROOT.ML";

+This directory contains the ML sources of the Isabelle system for +Higher-Order Logic.

Makefile -

compiles the files under Poly/ML or SML of New Jersey

- -

There are several subdirectories. To execute them, issue the command -

-        use_dir "<DIR>";
-

-where <DIR> is the desired directory - +There are several subdirectories with examples:

ex

general examples diff -r 636322bfd057 -r 815ef5848324 src/HOL/ex/README.html --- a/src/HOL/ex/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/HOL/ex/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,5 +1,5 @@ -HOL/ex/ReadMe +HOL/ex/README

ex--Miscellaneous Examples

diff -r 636322bfd057 -r 815ef5848324 src/HOLCF/IOA/README.html --- a/src/HOLCF/IOA/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/HOLCF/IOA/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,15 +1,11 @@ -HOLCF/ReadMe +HOLCF/IOA/README

IOA: A formalization of I/O automata in HOLCF

-Author: Olaf Mueller
+Author: Olaf Müller
Copyright 1997 Technische Universität München

-Version: 1.0
-Date: 1.05.97

- -The distribution contains - +The distribution contains:

A semantic model of the meta theory of I/O automata including proofs for the refinement notion and the compositionality of the model. For details see:
diff -r 636322bfd057 -r 815ef5848324 src/HOLCF/README.html --- a/src/HOLCF/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/HOLCF/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,14 +1,11 @@ -HOLCF/ReadMe +HOLCF/README -
HOLCF: A higher order version of LCF based on Isabelle HOL
+
HOLCF: A higher-order version of LCF based on Isabelle/HOL
Author: Franz Regensburger
Copyright 1995 Technische Universität München
-Version: 2.0
-Date: 16.08.95
- -A detailed description (in german) of the entire development can be found in +A detailed description (in german) of the entire development can be found in:
- HOLCF: eine konservative Erweiterung von HOL um LCF,
  @@ -18,29 +15,9 @@ Year: 1994.
-A short survey is available in +A short survey is available in:
- HOLCF: Higher Order Logic of Computable Functions
-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 symbolic font support -
- - - diff -r 636322bfd057 -r 815ef5848324 src/LCF/README.html --- a/src/LCF/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/LCF/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,24 +1,13 @@ -LCF/ReadMe +LCF/README
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 -Isabelle and type: use "ROOT.ML";
+This directory contains the ML sources of the Isabelle system for +LCF, based on FOL.
-
Makefile -
compiles the files under Poly/ML or SML of New Jersey
+The ex subdirectory contains some examples.
-
ex.ML -
file containing examples. To execute it, enter an ML image -containing LCF and type: use "ex.ML"; -
- -Useful references on First-Order Logic: +Useful references on LCF:
- Lawrence C. Paulson,
  diff -r 636322bfd057 -r 815ef5848324 src/Provers/README --- a/src/Provers/README Wed May 21 17:11:46 1997 +0200 +++ b/src/Provers/README Wed May 21 17:13:00 1997 +0200 @@ -2,14 +2,16 @@ This directory contains ML sources of generic theorem proving tools. Typically, they can be applied to various logics, provided rules of a -certain form are derivable. The first three are documented in the +certain form are derivable. Some of these are documented in the Reference Manual. -classical.ML -- theorem prover for classical logics -hypsubst.ML -- tactic to substitute in the hypotheses -simplifier.ML -- fast simplifier -simp.ML -- powerful but slow simplifier -typedsimp.ML -- basic simplifier for explicitly typed logics -splitter.ML -- performs case splits for simplifier.ML -genelim.ML -- bits and pieces for deriving elimination rules -ind.ML -- a simple induction package +blast.ML -- generic tableau prover with proof reconstruction +classical.ML -- theorem prover for classical logics +genelim.ML -- bits and pieces for deriving elimination rules +hypsubst.ML -- tactic to substitute in the hypotheses +ind.ML -- a simple induction package +nat_transitive.ML -- simple package for inequalities over nat +simp.ML -- powerful but slow simplifier +simplifier.ML -- fast simplifier +splitter.ML -- performs case splits for simplifier.ML +typedsimp.ML -- basic simplifier for explicitly typed logics diff -r 636322bfd057 -r 815ef5848324 src/Pure/README --- a/src/Pure/README Wed May 21 17:11:46 1997 +0200 +++ b/src/Pure/README Wed May 21 17:13:00 1997 +0200 @@ -3,16 +3,10 @@ This directory contains the ML source files for Pure Isabelle, which is the basis for all object-logics. Important files include: -Makefile -- compiles the files under Poly/ML or SML of New Jersey +IsaMakefile -- compiles the files -Syntax/ -- subdirectory containing the syntax module - -Thy/ -- subdirectory containing the thy file parser and loader +Syntax/ -- the syntax module -ROOT.ML -- loads all source files. Enter ML and type: use "ROOT.ML"; +Thy/ -- the theory file parser and loader -NJ.ML -- compatibility file for Standard ML of New Jersey. You may wish to - alter the parameter settings. - -POLY.ML -- compatibility file for Poly/ML - +ML-Systems/ -- compatibility files for various ML systems diff -r 636322bfd057 -r 815ef5848324 src/Pure/Syntax/README --- a/src/Pure/Syntax/README Wed May 21 17:11:46 1997 +0200 +++ b/src/Pure/Syntax/README Wed May 21 17:13:00 1997 +0200 @@ -10,6 +10,5 @@ Syntax (internal interface to the syntax module) BasicSyntax (part of Syntax made pervasive) -There is no Makefile to compile these files separately; they are compiled as -part of Pure Isabelle. - +There is no IsaMakefile to compile these files separately; they are +compiled as part of Pure Isabelle. diff -r 636322bfd057 -r 815ef5848324 src/Sequents/README.html --- a/src/Sequents/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/Sequents/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,37 +1,15 @@ -Sequents/ReadMe +Sequents/README
  Sequents: Various Sequent Calculi
  -This directory contains the Standard ML sources of the Isabelle system for -various Sequent, Linear, and Modal Logic. 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 - +This directory contains the ML sources of the Isabelle system for +various Sequent, Linear, and Modal Logic.
  -
  ex -
  subdirectory containing examples. Files are arranged in -subdirectories. To execute all of them, enter an ML image containing -Sequents and type -
```
-	use "ex/ROOT.ML";
-
```
  -To execute examples in a particular logic (LK/ILL/Modal) use the -appropriate command: -
```
-	use "ex/LK/ROOT.ML";
-	use "ex/ILL/ROOT.ML";
-	use "ex/Modal/ROOT.ML";
-
```
  -
  +The subdirectories ex, ex/LK, ex/ILL, +ex/Modal contain some examples.
  -
  Much of the work in Modal logic was done by Martin Coen. Thanks to +Much of the work in Modal logic was done by Martin Coen. Thanks to Rajeev Gore' for supplying the inference system for S43. Sara Kalvala reorganized the files and supplied Linear Logic. Jacob Frost provided some improvements to the syntax of sequents. diff -r 636322bfd057 -r 815ef5848324 src/Tools/README --- a/src/Tools/README Wed May 21 17:11:46 1997 +0200 +++ b/src/Tools/README Wed May 21 17:13:00 1997 +0200 @@ -1,3 +1,11 @@ + +*************************************************************************** + +IMPORTANT NOTE: These tools will disappear next time! + +*************************************************************************** + + Tools: Shell scripts and utilities associated with Isabelle To make these tools visible, you may wish to add this directory to your PATH diff -r 636322bfd057 -r 815ef5848324 src/ZF/AC/README.html --- a/src/ZF/AC/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/ZF/AC/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,5 +1,5 @@ -ZF/AC +ZF/AC/README
  AC -- Equivalents of the Axiom of Choice
  @@ -19,11 +19,5 @@ Mechanizing Set Theory, by Paulson and Grabczewski, describes both this development and ZF's theories of cardinals.
  -
  - -
  Last modified 5 March 1996 - -
  -
  Lawrence C. Paulson / -lcp@cl.cam.ac.uk -
  + + diff -r 636322bfd057 -r 815ef5848324 src/ZF/Coind/README.html --- a/src/ZF/Coind/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/ZF/Coind/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,5 +1,5 @@ -ZF/Coind +ZF/Coind/README
  Coind -- A Coinduction Example
  @@ -26,13 +26,6 @@ Frost's report describes this development. -
  -
  - -
  Last modified 5 March 1996 - -
  -
  Lawrence C. Paulson / -lcp@cl.cam.ac.uk -
  + + diff -r 636322bfd057 -r 815ef5848324 src/ZF/IMP/README.html --- a/src/ZF/IMP/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/ZF/IMP/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,5 +1,5 @@ -ZF/IMP +ZF/IMP/README
  IMP -- A while-language and two semantics
  @@ -23,16 +23,3 @@ A much extended version of this development is found in HOL/IMP. - -
  - -
  Last modified 5 March 1996 - -
  -
  Lawrence C. Paulson / -lcp@cl.cam.ac.uk - -
  -Tobias Nipkow / Tobias.Nipkow@informatik.tu-muenchen.de -
  diff -r 636322bfd057 -r 815ef5848324 src/ZF/README.html --- a/src/ZF/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/ZF/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,25 +1,11 @@ -ZF/ReadMe +ZF/README
  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.
  +This directory contains the ML sources of the Isabelle system for +ZF Set Theory, based on FOL.
  -
  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"; - +There are several subdirectories of examples:
  
  AC
  subdirectory containing proofs from the book "Equivalents of the Axiom diff -r 636322bfd057 -r 815ef5848324 src/ZF/Resid/README.html --- a/src/ZF/Resid/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/ZF/Resid/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,5 +1,5 @@ -ZF/Resid +ZF/Resid/README
  Resid -- A theory of residuals
  @@ -20,14 +20,8 @@ See Rasmussen's report -The Church-Rosser Theorem in Isabelle: A Proof Porting +The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment. -
  - -
  Last modified 5 March 1996 - -
  -
  Lawrence C. Paulson / -lcp@cl.cam.ac.uk -
  + + diff -r 636322bfd057 -r 815ef5848324 src/ZF/ex/README.html --- a/src/ZF/ex/README.html Wed May 21 17:11:46 1997 +0200 +++ b/src/ZF/ex/README.html Wed May 21 17:13:00 1997 +0200 @@ -1,5 +1,5 @@ -ZF/ex +ZF/ex/README
  ZF general examples
  @@ -10,11 +10,5 @@
  Several (co)inductive and (co)datatype definitions are presented. One report describes the theoretical foundations of datatypes while another describes the package that automates their declaration. -
  - -
  Last modified 5 March 1996 - -
  -
  Lawrence C. Paulson / -lcp@cl.cam.ac.uk -
  + +

CTT: Constructive Type Theory

Cube: Barendregt's Lambda-Cube

FOL: First-Order Logic with Natural Deduction

Axiomatic type classes

IOA: A basic formalization of I/O automata in HOL

A Simplified Scanner Generator

M.Sc./Diplom/Fopra Project

Invoking Model Checkers in Isabelle/HOL

HOL: Higher-Order Logic with curried functions

HOL: Higher-Order Logic

ex--Miscellaneous Examples

IOA: A formalization of I/O automata in HOLCF

HOLCF: A higher order version of LCF based on Isabelle HOL

HOLCF: A higher-order version of LCF based on Isabelle/HOL

LCF: Logic for Computable Functions

Sequents: Various Sequent Calculi

AC -- Equivalents of the Axiom of Choice

Coind -- A Coinduction Example

IMP -- A while-language and two semantics

ZF: Zermelo-Fraenkel Set Theory

Resid -- A theory of residuals

ZF general examples

IMP -- A `while`-language and two semantics