--- a/src/Modal/README.html Thu Oct 10 11:09:03 1996 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-<HTML><HEAD><TITLE>Modal/ReadMe</TITLE></HEAD><BODY>
-
-<H2>Modal: First-Order Modal Sequent Calculus</H2>
-
-This directory contains the Standard ML sources of the Isabelle system for
-Modal Logic. Important files include
-
-<DL>
-<DT>ROOT.ML
-<DD>loads all source files. Enter an ML image containing LK
-Isabelle and type: use "ROOT.ML";<P>
-
-<DT>ex
-<DD>subdirectory containing examples. Files Tthms.ML, S4thms.ML and
-S43thms.ML contain the theorems of Modal Logics, so arranged since
-T<S4<S43. To execute them, enter an ML image containing Modal
-and type: use "ex/ROOT.ML";
-</DL>
-
-Thanks to Rajeev Gore' for supplying the inference system for S43.<P>
-
-Useful references on Modal Logics:
-
-<UL>
-<LI>Melvin C Fitting,<BR>
- Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
-<LI>Lincoln A. Wallen,<BR>
- Automated Deduction in Nonclassical Logics (MIT Press, 1990)
-</UL>
-</BODY></HTML>