src/Sequents/README.html
changeset 3279 815ef5848324
parent 2073 fb0655539d05
child 5383 74c2da44d144
     1.1 --- a/src/Sequents/README.html	Wed May 21 17:11:46 1997 +0200
     1.2 +++ b/src/Sequents/README.html	Wed May 21 17:13:00 1997 +0200
     1.3 @@ -1,37 +1,15 @@
     1.4  <!-- $Id$ -->
     1.5 -<HTML><HEAD><TITLE>Sequents/ReadMe</TITLE></HEAD><BODY>
     1.6 +<HTML><HEAD><TITLE>Sequents/README</TITLE></HEAD><BODY>
     1.7  
     1.8  <H2>Sequents: Various Sequent Calculi</H2>
     1.9  
    1.10 -This directory contains the Standard ML sources of the Isabelle system for
    1.11 -various Sequent, Linear, and Modal Logic.  Important files include
    1.12 -
    1.13 -<DL>
    1.14 -<DT>ROOT.ML
    1.15 -<DD>loads all source files.  Enter an ML image containing Pure
    1.16 -Isabelle and type:    use "ROOT.ML";
    1.17 -
    1.18 -<DT>Makefile
    1.19 -<DD>compiles the files under Poly/ML or SML of New Jersey
    1.20 -
    1.21 +This directory contains the ML sources of the Isabelle system for
    1.22 +various Sequent, Linear, and Modal Logic.<p>
    1.23  
    1.24 -<DT>ex
    1.25 -<DD>subdirectory containing examples.  Files are arranged in
    1.26 -subdirectories. To execute all of them, enter an ML image containing
    1.27 -Sequents and type 
    1.28 -<PRE>
    1.29 -	use "ex/ROOT.ML";
    1.30 -</PRE>
    1.31 -To execute examples in a particular logic (LK/ILL/Modal) use the
    1.32 -appropriate command:
    1.33 -<PRE>
    1.34 -	use "ex/LK/ROOT.ML";
    1.35 -	use "ex/ILL/ROOT.ML";
    1.36 -	use "ex/Modal/ROOT.ML";
    1.37 -</PRE>
    1.38 -</DL>
    1.39 +The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>,
    1.40 +<tt>ex/Modal</tt> contain some examples.<p>
    1.41  
    1.42 -<P>Much of the work in Modal logic was done by Martin Coen. Thanks to
    1.43 +Much of the work in Modal logic was done by Martin Coen. Thanks to
    1.44  Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
    1.45  reorganized the files and supplied Linear Logic. Jacob Frost provided
    1.46  some improvements to the syntax of sequents.