changeset 1341 69fec018854c
child 3279 815ef5848324
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LCF/README.html	Fri Nov 17 13:22:50 1995 +0100
@@ -0,0 +1,27 @@
+<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
+<DD>loads all source files.  Enter an ML image containing FOL
+Isabelle and type: use "ROOT.ML";<P>
+<DD>compiles the files under Poly/ML or SML of New Jersey<P>
+<DD>file containing examples.  To execute it, enter an ML image
+containing LCF and type:    use "ex.ML";
+Useful references on First-Order Logic:
+<LI>Lawrence C. Paulson,<BR>
+    Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)