--- a/src/Sequents/README.html Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <TITLE>Sequents/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H2>Sequents: Various Sequent Calculi</H2>
-
-This directory contains the ML sources of the Isabelle system for
-various Sequent, Linear, and Modal Logic.<p>
-
-The subdirectories <tt>ex</tt>, <tt>ex/LK</tt>, <tt>ex/ILL</tt>,
-<tt>ex/Modal</tt> contain some examples.<p>
-
-Much of the work in Modal logic was done by Martin Coen. Thanks to
-Rajeev Gore' for supplying the inference system for S43. Sara Kalvala
-reorganized the files and supplied Linear Logic. Jacob Frost provided
-some improvements to the syntax of sequents.
-
-<P>Useful references on sequent calculi:
-
-<UL>
-<LI>Steve Reeves and Michael Clarke,<BR>
- Logic for Computer Science (Addison-Wesley, 1990)
-<LI>G. Takeuti,<BR>
- Proof Theory (North Holland, 1987)
-</UL>
-
-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>
-
-Useful references on Linear Logic:
-<UL>
-<LI>A. S. Troelstra<BR>
- Lectures on Linear Logic (CSLI, 1992)
-
-<LI>S. Kalvala and V. de Paiva<BR>
- Linear Logic in Isabelle (in TR 379, University of Cambridge
- Computer Lab, 1995, ed L. Paulson)
-</UL>
-
-</BODY></HTML>