--- 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.