Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned all READMEs;
authorwenzelm
Wed, 21 May 1997 17:13:00 +0200
changeset 3279 815ef5848324
parent 3278 636322bfd057
child 3280 87e734c72152
tuned all READMEs;
README.html file | annotate | diff | comparison | revisions
src/CTT/README.html file | annotate | diff | comparison | revisions
src/Cube/README.html file | annotate | diff | comparison | revisions
src/FOL/README.html file | annotate | diff | comparison | revisions
src/HOL/AxClasses/README.html file | annotate | diff | comparison | revisions
src/HOL/IOA/README.html file | annotate | diff | comparison | revisions
src/HOL/Lex/README.html file | annotate | diff | comparison | revisions
src/HOL/Modelcheck/README.html file | annotate | diff | comparison | revisions
src/HOL/README.html file | annotate | diff | comparison | revisions
src/HOL/ex/README.html file | annotate | diff | comparison | revisions
src/HOLCF/IOA/README.html file | annotate | diff | comparison | revisions
src/HOLCF/README.html file | annotate | diff | comparison | revisions
src/LCF/README.html file | annotate | diff | comparison | revisions
src/Provers/README file | annotate | diff | comparison | revisions
src/Pure/README file | annotate | diff | comparison | revisions
src/Pure/Syntax/README file | annotate | diff | comparison | revisions
src/Sequents/README.html file | annotate | diff | comparison | revisions
src/Tools/README file | annotate | diff | comparison | revisions
src/ZF/AC/README.html file | annotate | diff | comparison | revisions
src/ZF/Coind/README.html file | annotate | diff | comparison | revisions
src/ZF/IMP/README.html file | annotate | diff | comparison | revisions
src/ZF/README.html file | annotate | diff | comparison | revisions
src/ZF/Resid/README.html file | annotate | diff | comparison | revisions
src/ZF/ex/README.html file | annotate | diff | comparison | revisions 
--- 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:
 <ul>
 <li> A full Standard ML Compiler (e.g. Poly/ML or SML of New Jersey).
-<li> The GNU bash shell (version 1.14.x or 2.x).
+<li> The GNU bash shell (version 1.x or 2.x).
 <li> Perl 5.x - the Pathologically Eclectic Rubbish Lister.
 </ul>
 
@@ -44,8 +44,7 @@
 The following ML system and platform combinations are known to work
 quite well:
 <ul>
-<li> Poly/ML versions 2.x and 3.1 on Suns (running SunOS 4.1.x or
-Solaris 2.x).
+<li> Poly/ML versions 2.x and 3.1 on Suns.
 <li> SML/NJ 0.93 on Suns and SGIs. There seem to be several
 problems with Linux and HP-UX.
 <li> SML/NJ 1.07 on Suns, Linux, etc.
--- 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 @@
-<HTML><HEAD><TITLE>CTT/ReadMe</TITLE></HEAD><BODY>
+
+<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
+This directory contains the ML sources of the Isabelle system for
+Constructive Type Theory (extensional equality, no universes).<p>
 
-<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>
+The <tt>ex</tt> subdirectory contains some examples.<p>
 
 Useful references on Constructive Type Theory:
 
@@ -29,4 +18,6 @@
 <LI>	Simon Thompson,<BR>
 	Type Theory and Functional Programming (Addison-Wesley, 1991)
 </UL>
-</BODY></HTML>
+
+</BODY>
+</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 @@
-<HTML><HEAD><TITLE>Cube/ReadMe</TITLE></HEAD><BODY>
+
+<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>
+This directory contains the ML sources of the Isabelle system for the
+Lambda-Cube.<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>
+The <tt>ex</tt> subdirectory contains some examples.<p>
 
 NB: the formalization is not completely sound!  It does not enforce
 distinctness of variable names in contexts!<P>
@@ -28,4 +18,5 @@
     Introduction to Generalised Type Systems<BR>
     J. Functional Programming
 </UL>
-</BODY></HTML>
+</BODY>
+</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 @@
-<HTML><HEAD><TITLE>FOL/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>FOL/README</TITLE></HEAD><BODY>
 
 <H2>FOL: First-Order Logic with Natural Deduction</H2>
 
-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.<p>
 
-<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 FOL and type: use "ex/ROOT.ML";<P>
-</DL>
+The <tt>ex</tt> subdirectory contains some examples.<p>
 
 Useful references on First-Order Logic:
 
 <UL>
+<LI> Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, 1991)<br>
+ (The first chapter is an excellent introduction to natural
+deduction in general.)
 <LI>Antony Galton, Logic for Information Technology (Wiley, 1990)
 <LI>Michael Dummett, Elements of Intuitionism (Oxford, 1977)
 </UL>
--- 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 @@
-<HTML><HEAD><TITLE>HOL/AxClasses/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>HOL/AxClasses/README</TITLE></HEAD><BODY>
+
+<h2>Axiomatic type classes</h2>
 
 This directory contains the following axiomatic type class examples:
 
--- 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 @@
-<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
 
 <H3>IOA: A basic formalization of I/O automata in HOL</H3>
 
--- 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 @@
-<HTML><HEAD><TITLE>HOL/Lex/ReadMe</TITLE></HEAD>
+<HTML><HEAD><TITLE>HOL/Lex/README</TITLE></HEAD>
 <BODY>
 
 <H1>A Simplified Scanner Generator</H1>
@@ -34,15 +34,5 @@
 diagram, i.e. the translation of regular expressions into deterministic
 finite automata is still missing.  <P>
 
-<H2>M.Sc./Diplom/Fopra Project</H2>
-
-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 <A
-HREF="http://www4.informatik.tu-muenchen.de/~nipkow/">Tobias Nipkow</A> or <A
-HREF="http://www4.informatik.tu-muenchen.de/~pusch/">Cornelia Pusch</A>.
-This project is also suitable as a joint "Fopra" for two students.
-
 </BODY>
 </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 @@
 
 <H3>Invoking Model Checkers in Isabelle/HOL </H3>
 
-Authors:     Olaf Mueller, Jan Philipps, Robert Sandner<BR>
+Authors:     Olaf M&uuml;ller, Jan Philipps, Robert Sandner<BR>
 Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
 
 
--- 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 @@
 <!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
 
-<H2>HOL: Higher-Order Logic with curried functions</H2>
-
-This directory contains the Standard ML sources of the Isabelle system for
-Higher-Order Logic with curried functions.  Important files include
+<H2>HOL: Higher-Order Logic</H2>
 
-<DL>
-<DT>ROOT.ML
-<DD>loads all source files.  Enter an ML image containing Pure
-Isabelle and type: use "ROOT.ML";<P>
+This directory contains the ML sources of the Isabelle system for
+Higher-Order Logic.<P>
 
-<DT>Makefile
-<DD>compiles the files under Poly/ML or SML of New Jersey<P>
-</DL>
-
-<P>There are several subdirectories.  To execute them, issue the command
-<PRE>
-        use_dir "<I>&lt;DIR&gt;</I>";
-</PRE>
-where <I>&lt;DIR&gt;</I> is the desired directory 
-
+There are several subdirectories with examples:
 <DL>
 <DT>ex
 <DD>general examples
--- 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 @@
 <!-- $Id$ -->
-<HTML><HEAD><TITLE>HOL/ex/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>HOL/ex/README</TITLE></HEAD><BODY>
 
 <H2>ex--Miscellaneous Examples</H2>
 
--- 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 @@
-<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
 
 <H3>IOA: A formalization of I/O automata in HOLCF</H3>
 
-Author:     Olaf Mueller<BR>
+Author:     Olaf M&uuml;ller<BR>
 Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
 
-Version: 1.0<BR>
-Date: 1.05.97<P>
-
-The distribution contains
-
+The distribution contains:
 <UL>
   <li> 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: <BR>
--- 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 @@
-<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
 
-<H3>HOLCF: A higher order version of LCF based on Isabelle HOL</H3>
+<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
 
 Author:     Franz Regensburger<BR>
 Copyright   1995 Technische Universität München<P>
 
-Version: 2.0<BR>
-Date: 16.08.95<P>
-
-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:
 
 <UL>
   <li> <A HREF="http://www4.informatik.tu-muenchen.de/papers/Diss_Regensbu.ps.gz"> HOLCF: eine konservative Erweiterung von HOL um LCF</A>, <br>
@@ -18,29 +15,9 @@
         Year: 1994.
 </UL>
 
-A short survey is available in
+A short survey is available in:
 <UL>
 <li><A HREF="http://www4.informatik.tu-muenchen.de/papers/Regensburger_HOLT1995.ps.gz">HOLCF: Higher Order Logic of Computable Functions</A> <br>
 </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, generated
-    and optional 8bit symbolic font support
-</DL>
 </BODY></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 @@
-<HTML><HEAD><TITLE>LCF/ReadMe</TITLE></HEAD><BODY>
+<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>
+This directory contains the ML sources of the Isabelle system for
+LCF, based on FOL.<p>
 
-<DT>Makefile
-<DD>compiles the files under Poly/ML or SML of New Jersey<P>
+The <tt>ex</tt> subdirectory contains some examples.<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:
+Useful references on LCF:
 
 <UL>
 <LI>Lawrence C. Paulson,<BR>
--- 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
--- 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
--- 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.
--- 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 @@
 <!-- $Id$ -->
-<HTML><HEAD><TITLE>Sequents/ReadMe</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>Sequents/README</TITLE></HEAD><BODY>
 
 <H2>Sequents: Various Sequent Calculi</H2>
 
-This directory contains the Standard ML sources of the Isabelle system for
-various Sequent, Linear, and Modal Logic.  Important files include
-
-<DL>
-<DT>ROOT.ML
-<DD>loads all source files.  Enter an ML image containing Pure
-Isabelle and type:    use "ROOT.ML";
-
-<DT>Makefile
-<DD>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.<p>
 
-<DT>ex
-<DD>subdirectory containing examples.  Files are arranged in
-subdirectories. To execute all of them, enter an ML image containing
-Sequents and type 
-<PRE>
-	use "ex/ROOT.ML";
-</PRE>
-To execute examples in a particular logic (LK/ILL/Modal) use the
-appropriate command:
-<PRE>
-	use "ex/LK/ROOT.ML";
-	use "ex/ILL/ROOT.ML";
-	use "ex/Modal/ROOT.ML";
-</PRE>
-</DL>
+The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>,
+<tt>ex/Modal</tt> contain some examples.<p>
 
-<P>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.
--- 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
--- 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 @@
 <!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/AC</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>ZF/AC/README</TITLE></HEAD><BODY>
 
 <H2>AC -- Equivalents of the Axiom of Choice</H2>
 
@@ -19,11 +19,5 @@
 <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.
 <P>
 
-<HR>
-
-<P>Last modified 5 March 1996
-
-<ADDRESS>
-<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
+</body>
+</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 @@
 <!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/Coind</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>ZF/Coind/README</TITLE></HEAD><BODY>
 
 <H2>Coind -- A Coinduction Example</H2>
 
@@ -26,13 +26,6 @@
 Frost's
 <A
 HREF="http://www.cl.cam.ac.uk/Research/Reports/TR359-jf10008-co-induction-in-isabelle.dvi.gz">report</A> describes this development.
-<P>
 
-<HR>
-
-<P>Last modified 5 March 1996
-
-<ADDRESS>
-<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
+</body>
+</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 @@
 <!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/IMP</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>ZF/IMP/README</TITLE></HEAD><BODY>
 
 <H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2>
 
@@ -23,16 +23,3 @@
 A much extended version of this development is found in
 <A HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
 </BODY></HTML>
-
-<HR>
-
-<P>Last modified 5 March 1996
-
-<ADDRESS>
-<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-
-<P>
-<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/">Tobias Nipkow</A> / <A NAME="Tobias.Nipkow@informatik.tu-muenchen.de" 
-          HREF="mailto:Tobias.Nipkow@informatik.tu-muenchen.de">Tobias.Nipkow@informatik.tu-muenchen.de</A>
-</ADDRESS>
--- 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 @@
-<HTML><HEAD><TITLE>ZF/ReadMe</TITLE></HEAD><BODY>
+<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>
+This directory contains the ML sources of the Isabelle system for
+ZF Set Theory, based on FOL.<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 &lt;Dir&gt;, enter an ML image containing ZF and type
-<TT>use "&lt;Dir&gt;/ROOT.ML";</TT>
-
+There are several subdirectories of examples:
 <DL>
 <DT>AC
 <DD>subdirectory containing proofs from the book "Equivalents of the Axiom
--- 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 @@
 <!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/Resid</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>ZF/Resid/README</TITLE></HEAD><BODY>
 
 <H2>Resid -- A theory of residuals</H2>
 
@@ -20,14 +20,8 @@
 </PRE>
 
 See Rasmussen's report
-<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
+<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
 		  Experiment</A>.
 
-<HR>
-
-<P>Last modified 5 March 1996
-
-<ADDRESS>
-<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
+</body>
+</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 @@
 <!-- $Id$ -->
-<HTML><HEAD><TITLE>ZF/ex</TITLE></HEAD><BODY>
+<HTML><HEAD><TITLE>ZF/ex/README</TITLE></HEAD><BODY>
 
 <H2>ZF general examples</H2>
 
@@ -10,11 +10,5 @@
 
 <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.
 
-<HR>
-
-<P>Last modified 5 March 1996
-
-<ADDRESS>
-<P><A HREF="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</A> /
-<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
-</ADDRESS>
+</body>
+</html>
isabelle