--- /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
+
--- 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]]
--- /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
--- /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
+
--- /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
+
--- 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. *}
--- /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
+
--- /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
+