tuned all READMEs;
authorwenzelm
Wed May 21 17:13:00 1997 +0200 (1997-05-21)
changeset 3279815ef5848324
parent 3278 636322bfd057
child 3280 87e734c72152
tuned all READMEs;
README.html
src/CTT/README.html
src/Cube/README.html
src/FOL/README.html
src/HOL/AxClasses/README.html
src/HOL/IOA/README.html
src/HOL/Lex/README.html
src/HOL/Modelcheck/README.html
src/HOL/README.html
src/HOL/ex/README.html
src/HOLCF/IOA/README.html
src/HOLCF/README.html
src/LCF/README.html
src/Provers/README
src/Pure/README
src/Pure/Syntax/README
src/Sequents/README.html
src/Tools/README
src/ZF/AC/README.html
src/ZF/Coind/README.html
src/ZF/IMP/README.html
src/ZF/README.html
src/ZF/Resid/README.html
src/ZF/ex/README.html
     1.1 --- a/README.html	Wed May 21 17:11:46 1997 +0200
     1.2 +++ b/README.html	Wed May 21 17:13:00 1997 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  distribution:
     1.5  <ul>
     1.6  <li> A full Standard ML Compiler (e.g. Poly/ML or SML of New Jersey).
     1.7 -<li> The GNU bash shell (version 1.14.x or 2.x).
     1.8 +<li> The GNU bash shell (version 1.x or 2.x).
     1.9  <li> Perl 5.x - the Pathologically Eclectic Rubbish Lister.
    1.10  </ul>
    1.11  
    1.12 @@ -44,8 +44,7 @@
    1.13  The following ML system and platform combinations are known to work
    1.14  quite well:
    1.15  <ul>
    1.16 -<li> Poly/ML versions 2.x and 3.1 on Suns (running SunOS 4.1.x or
    1.17 -Solaris 2.x).
    1.18 +<li> Poly/ML versions 2.x and 3.1 on Suns.
    1.19  <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
    1.20  problems with Linux and HP-UX.
    1.21  <li> SML/NJ 1.07 on Suns, Linux, etc.
     2.1 --- a/src/CTT/README.html	Wed May 21 17:11:46 1997 +0200
     2.2 +++ b/src/CTT/README.html	Wed May 21 17:13:00 1997 +0200
     2.3 @@ -1,23 +1,12 @@
     2.4 -<HTML><HEAD><TITLE>CTT/ReadMe</TITLE></HEAD><BODY>
     2.5 +
     2.6 +<HTML><HEAD><TITLE>CTT/README</TITLE></HEAD><BODY>
     2.7  
     2.8  <H2>CTT: Constructive Type Theory</H2>
     2.9  
    2.10 -This directory contains the Standard ML sources of the Isabelle system for
    2.11 -Constructive Type Theory (extensional equality, no universes).  Important
    2.12 -files include
    2.13 +This directory contains the ML sources of the Isabelle system for
    2.14 +Constructive Type Theory (extensional equality, no universes).<p>
    2.15  
    2.16 -<DL>
    2.17 -<DT>ROOT.ML
    2.18 -<DD>loads all source files.  Enter an ML image containing Pure
    2.19 -Isabelle and type: use "ROOT.ML";<P>
    2.20 -
    2.21 -<DT>Makefile
    2.22 -<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    2.23 -
    2.24 -<DT>ex
    2.25 -<DD>subdirectory containing examples.  To execute them, enter an ML image
    2.26 -containing CTT and type: use "ex/ROOT.ML";<P>
    2.27 -</DL>
    2.28 +The <tt>ex</tt> subdirectory contains some examples.<p>
    2.29  
    2.30  Useful references on Constructive Type Theory:
    2.31  
    2.32 @@ -29,4 +18,6 @@
    2.33  <LI>	Simon Thompson,<BR>
    2.34  	Type Theory and Functional Programming (Addison-Wesley, 1991)
    2.35  </UL>
    2.36 -</BODY></HTML>
    2.37 +
    2.38 +</BODY>
    2.39 +</HTML>
     3.1 --- a/src/Cube/README.html	Wed May 21 17:11:46 1997 +0200
     3.2 +++ b/src/Cube/README.html	Wed May 21 17:13:00 1997 +0200
     3.3 @@ -1,22 +1,12 @@
     3.4 -<HTML><HEAD><TITLE>Cube/ReadMe</TITLE></HEAD><BODY>
     3.5 +
     3.6 +<HTML><HEAD><TITLE>Cube/README</TITLE></HEAD><BODY>
     3.7  
     3.8  <H2>Cube: Barendregt's Lambda-Cube</H2>
     3.9  
    3.10 -This directory contains the Standard ML sources of the Isabelle system for
    3.11 -the Lambda-Cube.  Important files include
    3.12 -
    3.13 -<DL>
    3.14 -<DT>ROOT.ML
    3.15 -<DD>loads all source files.  Enter an ML image containing Pure
    3.16 -Isabelle and type: use "ROOT.ML";<P>
    3.17 +This directory contains the ML sources of the Isabelle system for the
    3.18 +Lambda-Cube.<p>
    3.19  
    3.20 -<DT>Makefile
    3.21 -<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    3.22 -
    3.23 -<DT>ex
    3.24 -examples file. To execute them, enter an ML image
    3.25 -containing Cube and type: use "ex.ML";
    3.26 -</DL>
    3.27 +The <tt>ex</tt> subdirectory contains some examples.<p>
    3.28  
    3.29  NB: the formalization is not completely sound!  It does not enforce
    3.30  distinctness of variable names in contexts!<P>
    3.31 @@ -28,4 +18,5 @@
    3.32      Introduction to Generalised Type Systems<BR>
    3.33      J. Functional Programming
    3.34  </UL>
    3.35 -</BODY></HTML>
    3.36 +</BODY>
    3.37 +</HTML>
     4.1 --- a/src/FOL/README.html	Wed May 21 17:11:46 1997 +0200
     4.2 +++ b/src/FOL/README.html	Wed May 21 17:13:00 1997 +0200
     4.3 @@ -1,27 +1,19 @@
     4.4 -<HTML><HEAD><TITLE>FOL/ReadMe</TITLE></HEAD><BODY>
     4.5 +<HTML><HEAD><TITLE>FOL/README</TITLE></HEAD><BODY>
     4.6  
     4.7  <H2>FOL: First-Order Logic with Natural Deduction</H2>
     4.8  
     4.9 -This directory contains the Standard ML sources of the Isabelle system for
    4.10 -First-Order Logic (constructive and classical versions).  For a classical
    4.11 -sequent calculus, see LK.  Important files include
    4.12 +This directory contains the ML sources of the Isabelle system for
    4.13 +First-Order Logic (constructive and classical versions).  For a
    4.14 +classical sequent calculus, see LK.<p>
    4.15  
    4.16 -<DL>
    4.17 -<DT>ROOT.ML
    4.18 -<DD>loads all source files.  Enter an ML image containing Pure
    4.19 -Isabelle and type: use "ROOT.ML";<P>
    4.20 -
    4.21 -<DT>Makefile
    4.22 -<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    4.23 -
    4.24 -<DT>ex
    4.25 -<DD>subdirectory containing examples.  To execute them, enter an ML image
    4.26 -containing FOL and type: use "ex/ROOT.ML";<P>
    4.27 -</DL>
    4.28 +The <tt>ex</tt> subdirectory contains some examples.<p>
    4.29  
    4.30  Useful references on First-Order Logic:
    4.31  
    4.32  <UL>
    4.33 +<LI> Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 1991)<br>
    4.34 + (The first chapter is an excellent introduction to natural
    4.35 +deduction in general.)
    4.36  <LI>Antony Galton, Logic for Information Technology (Wiley, 1990)
    4.37  <LI>Michael Dummett, Elements of Intuitionism (Oxford, 1977)
    4.38  </UL>
     5.1 --- a/src/HOL/AxClasses/README.html	Wed May 21 17:11:46 1997 +0200
     5.2 +++ b/src/HOL/AxClasses/README.html	Wed May 21 17:13:00 1997 +0200
     5.3 @@ -1,4 +1,6 @@
     5.4 -<HTML><HEAD><TITLE>HOL/AxClasses/ReadMe</TITLE></HEAD><BODY>
     5.5 +<HTML><HEAD><TITLE>HOL/AxClasses/README</TITLE></HEAD><BODY>
     5.6 +
     5.7 +<h2>Axiomatic type classes</h2>
     5.8  
     5.9  This directory contains the following axiomatic type class examples:
    5.10  
     6.1 --- a/src/HOL/IOA/README.html	Wed May 21 17:11:46 1997 +0200
     6.2 +++ b/src/HOL/IOA/README.html	Wed May 21 17:13:00 1997 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
     6.5 +<HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
     6.6  
     6.7  <H3>IOA: A basic formalization of I/O automata in HOL</H3>
     6.8  
     7.1 --- a/src/HOL/Lex/README.html	Wed May 21 17:11:46 1997 +0200
     7.2 +++ b/src/HOL/Lex/README.html	Wed May 21 17:13:00 1997 +0200
     7.3 @@ -1,4 +1,4 @@
     7.4 -<HTML><HEAD><TITLE>HOL/Lex/ReadMe</TITLE></HEAD>
     7.5 +<HTML><HEAD><TITLE>HOL/Lex/README</TITLE></HEAD>
     7.6  <BODY>
     7.7  
     7.8  <H1>A Simplified Scanner Generator</H1>
     7.9 @@ -34,15 +34,5 @@
    7.10  diagram, i.e. the translation of regular expressions into deterministic
    7.11  finite automata is still missing.  <P>
    7.12  
    7.13 -<H2>M.Sc./Diplom/Fopra Project</H2>
    7.14 -
    7.15 -Task: formalize the translation of regular expressions into deterministic
    7.16 -finite automata. We are looking for a theoretically inclined student who
    7.17 -likes automata theory and is not afraid of logic and proofs.  Sounds
    7.18 -interesting? Then contact <A
    7.19 -HREF="http://www4.informatik.tu-muenchen.de/~nipkow/">Tobias Nipkow</A> or <A
    7.20 -HREF="http://www4.informatik.tu-muenchen.de/~pusch/">Cornelia Pusch</A>.
    7.21 -This project is also suitable as a joint "Fopra" for two students.
    7.22 -
    7.23  </BODY>
    7.24  </HTML>
     8.1 --- a/src/HOL/Modelcheck/README.html	Wed May 21 17:11:46 1997 +0200
     8.2 +++ b/src/HOL/Modelcheck/README.html	Wed May 21 17:13:00 1997 +0200
     8.3 @@ -2,7 +2,7 @@
     8.4  
     8.5  <H3>Invoking Model Checkers in Isabelle/HOL </H3>
     8.6  
     8.7 -Authors:     Olaf Mueller, Jan Philipps, Robert Sandner<BR>
     8.8 +Authors:     Olaf M&uuml;ller, Jan Philipps, Robert Sandner<BR>
     8.9  Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
    8.10  
    8.11  
     9.1 --- a/src/HOL/README.html	Wed May 21 17:11:46 1997 +0200
     9.2 +++ b/src/HOL/README.html	Wed May 21 17:13:00 1997 +0200
     9.3 @@ -1,26 +1,12 @@
     9.4  <!-- $Id$ -->
     9.5 -<HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>
     9.6 +<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
     9.7  
     9.8 -<H2>HOL: Higher-Order Logic with curried functions</H2>
     9.9 -
    9.10 -This directory contains the Standard ML sources of the Isabelle system for
    9.11 -Higher-Order Logic with curried functions.  Important files include
    9.12 +<H2>HOL: Higher-Order Logic</H2>
    9.13  
    9.14 -<DL>
    9.15 -<DT>ROOT.ML
    9.16 -<DD>loads all source files.  Enter an ML image containing Pure
    9.17 -Isabelle and type: use "ROOT.ML";<P>
    9.18 +This directory contains the ML sources of the Isabelle system for
    9.19 +Higher-Order Logic.<P>
    9.20  
    9.21 -<DT>Makefile
    9.22 -<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    9.23 -</DL>
    9.24 -
    9.25 -<P>There are several subdirectories.  To execute them, issue the command
    9.26 -<PRE>
    9.27 -        use_dir "<I>&lt;DIR&gt;</I>";
    9.28 -</PRE>
    9.29 -where <I>&lt;DIR&gt;</I> is the desired directory 
    9.30 -
    9.31 +There are several subdirectories with examples:
    9.32  <DL>
    9.33  <DT>ex
    9.34  <DD>general examples
    10.1 --- a/src/HOL/ex/README.html	Wed May 21 17:11:46 1997 +0200
    10.2 +++ b/src/HOL/ex/README.html	Wed May 21 17:13:00 1997 +0200
    10.3 @@ -1,5 +1,5 @@
    10.4  <!-- $Id$ -->
    10.5 -<HTML><HEAD><TITLE>HOL/ex/ReadMe</TITLE></HEAD><BODY>
    10.6 +<HTML><HEAD><TITLE>HOL/ex/README</TITLE></HEAD><BODY>
    10.7  
    10.8  <H2>ex--Miscellaneous Examples</H2>
    10.9  
    11.1 --- a/src/HOLCF/IOA/README.html	Wed May 21 17:11:46 1997 +0200
    11.2 +++ b/src/HOLCF/IOA/README.html	Wed May 21 17:13:00 1997 +0200
    11.3 @@ -1,15 +1,11 @@
    11.4 -<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
    11.5 +<HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
    11.6  
    11.7  <H3>IOA: A formalization of I/O automata in HOLCF</H3>
    11.8  
    11.9 -Author:     Olaf Mueller<BR>
   11.10 +Author:     Olaf M&uuml;ller<BR>
   11.11  Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
   11.12  
   11.13 -Version: 1.0<BR>
   11.14 -Date: 1.05.97<P>
   11.15 -
   11.16 -The distribution contains
   11.17 -
   11.18 +The distribution contains:
   11.19  <UL>
   11.20    <li> A semantic model of the meta theory of I/O automata including proofs for the refinement notion
   11.21         and the compositionality of the model. For details see: <BR>
    12.1 --- a/src/HOLCF/README.html	Wed May 21 17:11:46 1997 +0200
    12.2 +++ b/src/HOLCF/README.html	Wed May 21 17:13:00 1997 +0200
    12.3 @@ -1,14 +1,11 @@
    12.4 -<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
    12.5 +<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
    12.6  
    12.7 -<H3>HOLCF: A higher order version of LCF based on Isabelle HOL</H3>
    12.8 +<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
    12.9  
   12.10  Author:     Franz Regensburger<BR>
   12.11  Copyright   1995 Technische Universität München<P>
   12.12  
   12.13 -Version: 2.0<BR>
   12.14 -Date: 16.08.95<P>
   12.15 -
   12.16 -A detailed description (in german) of the entire development can be found in 
   12.17 +A detailed description (in german) of the entire development can be found in:
   12.18  
   12.19  <UL>
   12.20    <li> <A HREF="http://www4.informatik.tu-muenchen.de/papers/Diss_Regensbu.ps.gz"> HOLCF: eine konservative Erweiterung von HOL um LCF</A>, <br>
   12.21 @@ -18,29 +15,9 @@
   12.22          Year: 1994.
   12.23  </UL>
   12.24  
   12.25 -A short survey is available in
   12.26 +A short survey is available in:
   12.27  <UL>
   12.28  <li><A HREF="http://www4.informatik.tu-muenchen.de/papers/Regensburger_HOLT1995.ps.gz">HOLCF: Higher Order Logic of Computable Functions</A> <br>
   12.29  </UL>
   12.30  
   12.31 -Changes:
   12.32 -
   12.33 -<DL>
   12.34 -<DT>14.10.94
   12.35 -<DD>New translation mechanism for continuous infixes
   12.36 -
   12.37 -<DT>18.05.95
   12.38 -<DD>Conversion to curried version of HOL.
   12.39 -
   12.40 -<DT>28.06.95
   12.41 -<DD>The old uncurried version of HOLCF is no longer supported
   12.42 -    in the distribution.
   12.43 -
   12.44 -<DT>18.08.95
   12.45 -<DD>added sections axioms, ops, domain, generated
   12.46 -    and optional 8bit symbolic font support
   12.47 -</DL>
   12.48  </BODY></HTML>
   12.49 -
   12.50 -
   12.51 -
    13.1 --- a/src/LCF/README.html	Wed May 21 17:11:46 1997 +0200
    13.2 +++ b/src/LCF/README.html	Wed May 21 17:13:00 1997 +0200
    13.3 @@ -1,24 +1,13 @@
    13.4 -<HTML><HEAD><TITLE>LCF/ReadMe</TITLE></HEAD><BODY>
    13.5 +<HTML><HEAD><TITLE>LCF/README</TITLE></HEAD><BODY>
    13.6  
    13.7  <H2>LCF: Logic for Computable Functions</H2>
    13.8  
    13.9 -This directory contains the Standard ML sources of the Isabelle system for
   13.10 -LCF.  It is loaded upon FOL, not Pure Isabelle.  Important files include
   13.11 -
   13.12 -<DL>
   13.13 -<DT>ROOT.ML
   13.14 -<DD>loads all source files.  Enter an ML image containing FOL
   13.15 -Isabelle and type: use "ROOT.ML";<P>
   13.16 +This directory contains the ML sources of the Isabelle system for
   13.17 +LCF, based on FOL.<p>
   13.18  
   13.19 -<DT>Makefile
   13.20 -<DD>compiles the files under Poly/ML or SML of New Jersey<P>
   13.21 +The <tt>ex</tt> subdirectory contains some examples.<p>
   13.22  
   13.23 -<DT>ex.ML
   13.24 -<DD>file containing examples.  To execute it, enter an ML image
   13.25 -containing LCF and type:    use "ex.ML";
   13.26 -</DL>
   13.27 -
   13.28 -Useful references on First-Order Logic:
   13.29 +Useful references on LCF:
   13.30  
   13.31  <UL>
   13.32  <LI>Lawrence C. Paulson,<BR>
    14.1 --- a/src/Provers/README	Wed May 21 17:11:46 1997 +0200
    14.2 +++ b/src/Provers/README	Wed May 21 17:13:00 1997 +0200
    14.3 @@ -2,14 +2,16 @@
    14.4  
    14.5  This directory contains ML sources of generic theorem proving tools.
    14.6  Typically, they can be applied to various logics, provided rules of a
    14.7 -certain form are derivable.  The first three are documented in the
    14.8 +certain form are derivable.  Some of these are documented in the
    14.9  Reference Manual.
   14.10  
   14.11 -classical.ML  -- theorem prover for classical logics
   14.12 -hypsubst.ML   -- tactic to substitute in the hypotheses
   14.13 -simplifier.ML -- fast simplifier
   14.14 -simp.ML       -- powerful but slow simplifier
   14.15 -typedsimp.ML  -- basic simplifier for explicitly typed logics
   14.16 -splitter.ML   -- performs case splits for simplifier.ML
   14.17 -genelim.ML    -- bits and pieces for deriving elimination rules
   14.18 -ind.ML        -- a simple induction package
   14.19 +blast.ML          -- generic tableau prover with proof reconstruction
   14.20 +classical.ML      -- theorem prover for classical logics
   14.21 +genelim.ML        -- bits and pieces for deriving elimination rules
   14.22 +hypsubst.ML       -- tactic to substitute in the hypotheses
   14.23 +ind.ML            -- a simple induction package
   14.24 +nat_transitive.ML -- simple package for inequalities over nat
   14.25 +simp.ML           -- powerful but slow simplifier
   14.26 +simplifier.ML     -- fast simplifier
   14.27 +splitter.ML       -- performs case splits for simplifier.ML
   14.28 +typedsimp.ML      -- basic simplifier for explicitly typed logics
    15.1 --- a/src/Pure/README	Wed May 21 17:11:46 1997 +0200
    15.2 +++ b/src/Pure/README	Wed May 21 17:13:00 1997 +0200
    15.3 @@ -3,16 +3,10 @@
    15.4  This directory contains the ML source files for Pure Isabelle, which is the
    15.5  basis for all object-logics.  Important files include:
    15.6  
    15.7 -Makefile -- compiles the files under Poly/ML or SML of New Jersey
    15.8 +IsaMakefile -- compiles the files
    15.9  
   15.10 -Syntax/  -- subdirectory containing the syntax module
   15.11 -
   15.12 -Thy/     -- subdirectory containing the thy file parser and loader
   15.13 +Syntax/     -- the syntax module
   15.14  
   15.15 -ROOT.ML  -- loads all source files.  Enter ML and type:  use "ROOT.ML";
   15.16 +Thy/        -- the theory file parser and loader
   15.17  
   15.18 -NJ.ML    -- compatibility file for Standard ML of New Jersey.  You may wish to
   15.19 -            alter the parameter settings.
   15.20 -
   15.21 -POLY.ML  -- compatibility file for Poly/ML
   15.22 -
   15.23 +ML-Systems/ -- compatibility files for various ML systems
    16.1 --- a/src/Pure/Syntax/README	Wed May 21 17:11:46 1997 +0200
    16.2 +++ b/src/Pure/Syntax/README	Wed May 21 17:13:00 1997 +0200
    16.3 @@ -10,6 +10,5 @@
    16.4    Syntax        (internal interface to the syntax module)
    16.5    BasicSyntax   (part of Syntax made pervasive)
    16.6  
    16.7 -There is no Makefile to compile these files separately; they are compiled as
    16.8 -part of Pure Isabelle.
    16.9 -
   16.10 +There is no IsaMakefile to compile these files separately; they are
   16.11 +compiled as part of Pure Isabelle.
    17.1 --- a/src/Sequents/README.html	Wed May 21 17:11:46 1997 +0200
    17.2 +++ b/src/Sequents/README.html	Wed May 21 17:13:00 1997 +0200
    17.3 @@ -1,37 +1,15 @@
    17.4  <!-- $Id$ -->
    17.5 -<HTML><HEAD><TITLE>Sequents/ReadMe</TITLE></HEAD><BODY>
    17.6 +<HTML><HEAD><TITLE>Sequents/README</TITLE></HEAD><BODY>
    17.7  
    17.8  <H2>Sequents: Various Sequent Calculi</H2>
    17.9  
   17.10 -This directory contains the Standard ML sources of the Isabelle system for
   17.11 -various Sequent, Linear, and Modal Logic.  Important files include
   17.12 -
   17.13 -<DL>
   17.14 -<DT>ROOT.ML
   17.15 -<DD>loads all source files.  Enter an ML image containing Pure
   17.16 -Isabelle and type:    use "ROOT.ML";
   17.17 -
   17.18 -<DT>Makefile
   17.19 -<DD>compiles the files under Poly/ML or SML of New Jersey
   17.20 -
   17.21 +This directory contains the ML sources of the Isabelle system for
   17.22 +various Sequent, Linear, and Modal Logic.<p>
   17.23  
   17.24 -<DT>ex
   17.25 -<DD>subdirectory containing examples.  Files are arranged in
   17.26 -subdirectories. To execute all of them, enter an ML image containing
   17.27 -Sequents and type 
   17.28 -<PRE>
   17.29 -	use "ex/ROOT.ML";
   17.30 -</PRE>
   17.31 -To execute examples in a particular logic (LK/ILL/Modal) use the
   17.32 -appropriate command:
   17.33 -<PRE>
   17.34 -	use "ex/LK/ROOT.ML";
   17.35 -	use "ex/ILL/ROOT.ML";
   17.36 -	use "ex/Modal/ROOT.ML";
   17.37 -</PRE>
   17.38 -</DL>
   17.39 +The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>,
   17.40 +<tt>ex/Modal</tt> contain some examples.<p>
   17.41  
   17.42 -<P>Much of the work in Modal logic was done by Martin Coen. Thanks to
   17.43 +Much of the work in Modal logic was done by Martin Coen. Thanks to
   17.44  Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
   17.45  reorganized the files and supplied Linear Logic. Jacob Frost provided
   17.46  some improvements to the syntax of sequents.
    18.1 --- a/src/Tools/README	Wed May 21 17:11:46 1997 +0200
    18.2 +++ b/src/Tools/README	Wed May 21 17:13:00 1997 +0200
    18.3 @@ -1,3 +1,11 @@
    18.4 +
    18.5 +***************************************************************************
    18.6 +
    18.7 +IMPORTANT NOTE: These tools will disappear next time!
    18.8 +
    18.9 +***************************************************************************
   18.10 +
   18.11 +
   18.12  	Tools: Shell scripts and utilities associated with Isabelle
   18.13  
   18.14  To make these tools visible, you may wish to add this directory to your PATH
    19.1 --- a/src/ZF/AC/README.html	Wed May 21 17:11:46 1997 +0200
    19.2 +++ b/src/ZF/AC/README.html	Wed May 21 17:13:00 1997 +0200
    19.3 @@ -1,5 +1,5 @@
    19.4  <!-- $Id$ -->
    19.5 -<HTML><HEAD><TITLE>ZF/AC</TITLE></HEAD><BODY>
    19.6 +<HTML><HEAD><TITLE>ZF/AC/README</TITLE></HEAD><BODY>
    19.7  
    19.8  <H2>AC -- Equivalents of the Axiom of Choice</H2>
    19.9  
   19.10 @@ -19,11 +19,5 @@
   19.11  <A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz">Mechanizing Set Theory</A>, by Paulson and Grabczewski, describes both this development and ZF's theories of cardinals.
   19.12  <P>
   19.13  
   19.14 -<HR>
   19.15 -
   19.16 -<P>Last modified 5 March 1996
   19.17 -
   19.18 -<ADDRESS>
   19.19 -<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
   19.20 -<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   19.21 -</ADDRESS>
   19.22 +</body>
   19.23 +</html>
    20.1 --- a/src/ZF/Coind/README.html	Wed May 21 17:11:46 1997 +0200
    20.2 +++ b/src/ZF/Coind/README.html	Wed May 21 17:13:00 1997 +0200
    20.3 @@ -1,5 +1,5 @@
    20.4  <!-- $Id$ -->
    20.5 -<HTML><HEAD><TITLE>ZF/Coind</TITLE></HEAD><BODY>
    20.6 +<HTML><HEAD><TITLE>ZF/Coind/README</TITLE></HEAD><BODY>
    20.7  
    20.8  <H2>Coind -- A Coinduction Example</H2>
    20.9  
   20.10 @@ -26,13 +26,6 @@
   20.11  Frost's
   20.12  <A
   20.13  HREF="http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz">report</A> describes this development.
   20.14 -<P>
   20.15  
   20.16 -<HR>
   20.17 -
   20.18 -<P>Last modified 5 March 1996
   20.19 -
   20.20 -<ADDRESS>
   20.21 -<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
   20.22 -<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   20.23 -</ADDRESS>
   20.24 +</body>
   20.25 +</html>
    21.1 --- a/src/ZF/IMP/README.html	Wed May 21 17:11:46 1997 +0200
    21.2 +++ b/src/ZF/IMP/README.html	Wed May 21 17:13:00 1997 +0200
    21.3 @@ -1,5 +1,5 @@
    21.4  <!-- $Id$ -->
    21.5 -<HTML><HEAD><TITLE>ZF/IMP</TITLE></HEAD><BODY>
    21.6 +<HTML><HEAD><TITLE>ZF/IMP/README</TITLE></HEAD><BODY>
    21.7  
    21.8  <H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2>
    21.9  
   21.10 @@ -23,16 +23,3 @@
   21.11  A much extended version of this development is found in
   21.12  <A HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
   21.13  </BODY></HTML>
   21.14 -
   21.15 -<HR>
   21.16 -
   21.17 -<P>Last modified 5 March 1996
   21.18 -
   21.19 -<ADDRESS>
   21.20 -<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
   21.21 -<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   21.22 -
   21.23 -<P>
   21.24 -<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/">Tobias Nipkow</A> / <A NAME="Tobias.Nipkow@informatik.tu-muenchen.de" 
   21.25 -          HREF="mailto:Tobias.Nipkow@informatik.tu-muenchen.de">Tobias.Nipkow@informatik.tu-muenchen.de</A>
   21.26 -</ADDRESS>
    22.1 --- a/src/ZF/README.html	Wed May 21 17:11:46 1997 +0200
    22.2 +++ b/src/ZF/README.html	Wed May 21 17:13:00 1997 +0200
    22.3 @@ -1,25 +1,11 @@
    22.4 -<HTML><HEAD><TITLE>ZF/ReadMe</TITLE></HEAD><BODY>
    22.5 +<HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY>
    22.6  
    22.7  <H2>ZF: Zermelo-Fraenkel Set Theory</H2>
    22.8  
    22.9 -This directory contains the Standard ML sources of the Isabelle system for
   22.10 -ZF Set Theory.  It is loaded upon FOL, not Pure Isabelle.  Important files
   22.11 -include
   22.12 -
   22.13 -<DL>
   22.14 -<DT>Makefile
   22.15 -<DD>compiles the files under Poly/ML or SML of New Jersey.  Can also
   22.16 -run all the tests described below.<P>
   22.17 +This directory contains the ML sources of the Isabelle system for
   22.18 +ZF Set Theory, based on FOL.<p>
   22.19  
   22.20 -<DT>ROOT.ML
   22.21 -<DD>loads all source files.  Enter an ML image containing FOL and
   22.22 -type: use "ROOT.ML";
   22.23 -</DL>
   22.24 -
   22.25 -There are also several subdirectories of examples.  To execute the examples on
   22.26 -some directory &lt;Dir&gt;, enter an ML image containing ZF and type
   22.27 -<TT>use "&lt;Dir&gt;/ROOT.ML";</TT>
   22.28 -
   22.29 +There are several subdirectories of examples:
   22.30  <DL>
   22.31  <DT>AC
   22.32  <DD>subdirectory containing proofs from the book "Equivalents of the Axiom
    23.1 --- a/src/ZF/Resid/README.html	Wed May 21 17:11:46 1997 +0200
    23.2 +++ b/src/ZF/Resid/README.html	Wed May 21 17:13:00 1997 +0200
    23.3 @@ -1,5 +1,5 @@
    23.4  <!-- $Id$ -->
    23.5 -<HTML><HEAD><TITLE>ZF/Resid</TITLE></HEAD><BODY>
    23.6 +<HTML><HEAD><TITLE>ZF/Resid/README</TITLE></HEAD><BODY>
    23.7  
    23.8  <H2>Resid -- A theory of residuals</H2>
    23.9  
   23.10 @@ -20,14 +20,8 @@
   23.11  </PRE>
   23.12  
   23.13  See Rasmussen's report
   23.14 -<A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz">The Church-Rosser Theorem in Isabelle: A Proof Porting
   23.15 +<A HREF="http://www.cl.cam.ac.uk/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz">The Church-Rosser Theorem in Isabelle: A Proof Porting
   23.16  		  Experiment</A>.
   23.17  
   23.18 -<HR>
   23.19 -
   23.20 -<P>Last modified 5 March 1996
   23.21 -
   23.22 -<ADDRESS>
   23.23 -<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
   23.24 -<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   23.25 -</ADDRESS>
   23.26 +</body>
   23.27 +</html>
    24.1 --- a/src/ZF/ex/README.html	Wed May 21 17:11:46 1997 +0200
    24.2 +++ b/src/ZF/ex/README.html	Wed May 21 17:13:00 1997 +0200
    24.3 @@ -1,5 +1,5 @@
    24.4  <!-- $Id$ -->
    24.5 -<HTML><HEAD><TITLE>ZF/ex</TITLE></HEAD><BODY>
    24.6 +<HTML><HEAD><TITLE>ZF/ex/README</TITLE></HEAD><BODY>
    24.7  
    24.8  <H2>ZF general examples</H2>
    24.9  
   24.10 @@ -10,11 +10,5 @@
   24.11  
   24.12  <P>Several (co)inductive and (co)datatype definitions are presented.  <A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz">One report</A> describes the theoretical foundations of datatypes while <A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz">another</A> describes the package that automates their declaration.
   24.13  
   24.14 -<HR>
   24.15 -
   24.16 -<P>Last modified 5 March 1996
   24.17 -
   24.18 -<ADDRESS>
   24.19 -<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
   24.20 -<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   24.21 -</ADDRESS>
   24.22 +</body>
   24.23 +</html>