diff -r b05cd411d3d3 -r 2ff3a5589b05 src/Sequents/ROOT
--- a/src/Sequents/ROOT	Tue Mar 12 20:03:04 2013 +0100
+++ b/src/Sequents/ROOT	Tue Mar 12 21:59:48 2013 +0100
@@ -5,7 +5,37 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-    Classical Sequent Calculus based on Pure Isabelle.
+    Various Sequent Calculi for Classical, Linear, and Modal Logic.
+
+    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.
+
+
+    Useful references on sequent calculi:
+
+    Steve Reeves and Michael Clarke, Logic for Computer Science
+    (Addison-Wesley, 1990)
+
+    G. Takeuti, Proof Theory (North Holland, 1987)
+
+
+    Useful references on Modal Logics:
+
+    Melvin C Fitting, Proof Methods for Modal and Intuitionistic Logics
+    (Reidel, 1983)
+
+    Lincoln A. Wallen, Automated Deduction in Nonclassical Logics (MIT Press,
+    1990)
+
+
+    Useful references on Linear Logic:
+
+    A. S. Troelstra, Lectures on Linear Logic (CSLI, 1992)
+
+    S. Kalvala and V. de Paiva, Linear Logic in Isabelle (in TR 379, University
+    of Cambridge Computer Lab, 1995, ed L. Paulson)
   *}
   options [document = false]
   theories