--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LK/README.html	Fri Nov 17 13:22:50 1995 +0100
@@ -0,0 +1,30 @@
+<HTML><HEAD><TITLE>LK/ReadMe</TITLE></HEAD><BODY>
+
+<H2>LK: Classical First-Order Sequent Calculus</H2>
+
+This directory contains the Standard ML sources of the Isabelle system for
+First-Order Logic as a classical sequent calculus.  (For a Natural Deduction
+version, see FOL.)  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>
+
+<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 LK and type: use "ex/ROOT.ML";<P>
+</DL>
+
+Useful references on First-Order Logic:
+
+<UL>
+<LI>Jean Gallier,<BR>
+    Logic for Computer Science (Harper&Row, 1986)
+<LI>G. Takeuti,<BR>
+    Proof Theory (North Holland, 1987)
+</UL>
+</BODY></HTML>