# HG changeset patch
# User clasohm
# Date 816438477 -3600
# Node ID 70ee8d7b22330d42ff1d521fa9f8229913316b0a
# Parent e9becade00769a03d1b20af15ce4ee59de7c3447
HTML version of README
diff -r e9becade0076 -r 70ee8d7b2233 src/FOL/README.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/README.html Wed Nov 15 13:27:57 1995 +0100
@@ -0,0 +1,28 @@
+
FOL/ReadMe
+
+FOL: First-Order Logic with Natural Deduction
+
+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
+
+
+- ROOT.ML
+
- loads all source files. Enter an ML image containing Pure
+Isabelle and type: use "ROOT.ML";
+
+
- Makefile
+
- compiles the files under Poly/ML or SML of New Jersey
+
+
- ex
+
- subdirectory containing examples. To execute them, enter an ML image
+containing FOL and type: use "ex/ROOT.ML";
+
+
+Useful references on First-Order Logic:
+
+
+- Antony Galton, Logic for Information Technology (Wiley, 1990)
+
- Michael Dummett, Elements of Intuitionism (Oxford, 1977)
+
+