# HG changeset patch
# User wenzelm
# Date 1343131664 -7200
# Node ID 02dd825f5a4eaf5f41bd06fef36b9a8e59144b6b
# Parent  5b9d79c6323b0c0f8209abd7ed4642a172ce9782
more session ROOT files;

diff -r 5b9d79c6323b -r 02dd825f5a4e src/CCL/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CCL/ROOT	Tue Jul 24 14:07:44 2012 +0200
@@ -0,0 +1,21 @@
+session CCL! in "." = Pure +
+  description {*
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+    Classical Computational Logic based on First-Order Logic.
+
+    A computational logic for an untyped functional language with
+    evaluation to weak head-normal form.
+  *}
+  theories Wfd Fix
+
+session ex = CCL +
+  description {*
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+    Examples for Classical Computational Logic.
+  *}
+  theories Nat List Stream Flag
+
diff -r 5b9d79c6323b -r 02dd825f5a4e src/CCL/Set.thy
--- a/src/CCL/Set.thy	Tue Jul 24 13:22:06 2012 +0200
+++ b/src/CCL/Set.thy	Tue Jul 24 14:07:44 2012 +0200
@@ -1,7 +1,7 @@
 header {* Extending FOL by a modified version of HOL set theory *}
 
 theory Set
-imports FOL
+imports "~~/src/FOL/FOL"
 begin
 
 declare [[eta_contract]]
diff -r 5b9d79c6323b -r 02dd825f5a4e src/CTT/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/CTT/ROOT	Tue Jul 24 14:07:44 2012 +0200
@@ -0,0 +1,15 @@
+session CTT! in "." = Pure +
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+  *}
+  theories Main
+
+session ex = CTT +
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+
+    Examples for Constructive Type Theory.
+  *}
+  theories Typechecking Elimination Equality Synthesis
diff -r 5b9d79c6323b -r 02dd825f5a4e src/Cube/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/ROOT	Tue Jul 24 14:07:44 2012 +0200
@@ -0,0 +1,9 @@
+session Cube! in "." = Pure +
+  description {*
+    Author:     Tobias Nipkow
+    Copyright   1992  University of Cambridge
+
+    The Lambda-Cube a la Barendregt.
+  *}
+  theories Example
+
diff -r 5b9d79c6323b -r 02dd825f5a4e src/FOLP/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOLP/ROOT	Tue Jul 24 14:07:44 2012 +0200
@@ -0,0 +1,30 @@
+session FOLP! in "." = Pure +
+  description {*
+    Author:     Martin Coen, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+    Modifed version of FOL that contains proof terms.
+
+    Presence of unknown proof term means that matching does not behave as expected.
+  *}
+  theories FOLP
+
+session ex = FOLP +
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+    Examples for First-Order Logic.
+  *}
+  theories
+    Intro
+    Nat
+    Foundation
+    If
+    Intuitionistic
+    Classical
+    Propositional_Int
+    Quantifiers_Int
+    Propositional_Cla
+    Quantifiers_Cla
+
diff -r 5b9d79c6323b -r 02dd825f5a4e src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Tue Jul 24 13:22:06 2012 +0200
+++ b/src/LCF/LCF.thy	Tue Jul 24 14:07:44 2012 +0200
@@ -6,7 +6,7 @@
 header {* LCF on top of First-Order Logic *}
 
 theory LCF
-imports FOL
+imports "~~/src/FOL/FOL"
 begin
 
 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *}
diff -r 5b9d79c6323b -r 02dd825f5a4e src/LCF/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LCF/ROOT	Tue Jul 24 14:07:44 2012 +0200
@@ -0,0 +1,16 @@
+session LCF! in "." = Pure +
+  description {*
+    Author:     Tobias Nipkow
+    Copyright   1992  University of Cambridge
+  *}
+  theories LCF
+
+session ex = LCF +
+  description {*
+    Author:     Tobias Nipkow
+    Copyright   1991  University of Cambridge
+
+    Some examples from Lawrence Paulson's book Logic and Computation.
+  *}
+  theories Ex1 Ex2 Ex3 Ex4
+
diff -r 5b9d79c6323b -r 02dd825f5a4e src/Sequents/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Sequents/ROOT	Tue Jul 24 14:07:44 2012 +0200
@@ -0,0 +1,18 @@
+session Sequents! in "." = Pure +
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1991  University of Cambridge
+
+    Classical Sequent Calculus based on Pure Isabelle.
+  *}
+  theories LK ILL ILL_predlog Washing Modal0 T S4 S43
+
+session LK = Sequents +
+  description {*
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+    Examples for Classical Logic.
+  *}
+  theories Propositional Quantifiers Hard_Quantifiers Nat
+