# HG changeset patch
# User wenzelm
# Date 1391274028 -3600
# Node ID 08f2ebb6507891f1ee5ddbbcbe5b2dc4612e255b
# Parent  901a6696cdd8a963992a3c164b5e2b17ee91a60c
simplified sessions;

diff -r 901a6696cdd8 -r 08f2ebb65078 src/Sequents/LK/Hard_Quantifiers.thy
--- a/src/Sequents/LK/Hard_Quantifiers.thy	Sat Feb 01 17:56:03 2014 +0100
+++ b/src/Sequents/LK/Hard_Quantifiers.thy	Sat Feb 01 18:00:28 2014 +0100
@@ -12,7 +12,7 @@
 *)
 
 theory Hard_Quantifiers
-imports LK
+imports "../LK"
 begin
 
 lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
diff -r 901a6696cdd8 -r 08f2ebb65078 src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Sat Feb 01 17:56:03 2014 +0100
+++ b/src/Sequents/LK/Nat.thy	Sat Feb 01 18:00:28 2014 +0100
@@ -6,7 +6,7 @@
 header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
 
 theory Nat
-imports LK
+imports "../LK"
 begin
 
 typedecl nat
diff -r 901a6696cdd8 -r 08f2ebb65078 src/Sequents/LK/Propositional.thy
--- a/src/Sequents/LK/Propositional.thy	Sat Feb 01 17:56:03 2014 +0100
+++ b/src/Sequents/LK/Propositional.thy	Sat Feb 01 18:00:28 2014 +0100
@@ -6,7 +6,7 @@
 header {* Classical sequent calculus: examples with propositional connectives *}
 
 theory Propositional
-imports LK
+imports "../LK"
 begin
 
 text "absorptive laws of & and | "
diff -r 901a6696cdd8 -r 08f2ebb65078 src/Sequents/LK/Quantifiers.thy
--- a/src/Sequents/LK/Quantifiers.thy	Sat Feb 01 17:56:03 2014 +0100
+++ b/src/Sequents/LK/Quantifiers.thy	Sat Feb 01 18:00:28 2014 +0100
@@ -6,7 +6,7 @@
 *)
 
 theory Quantifiers
-imports LK
+imports "../LK"
 begin
 
 lemma "|- (ALL x. P)  <->  P"
diff -r 901a6696cdd8 -r 08f2ebb65078 src/Sequents/ROOT
--- a/src/Sequents/ROOT	Sat Feb 01 17:56:03 2014 +0100
+++ b/src/Sequents/ROOT	Sat Feb 01 18:00:28 2014 +0100
@@ -48,17 +48,9 @@
     S4
     S43
 
-session "Sequents-LK" in LK = Sequents +
-  description {*
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
+    (* Examples for Classical Logic *)
+    "LK/Propositional"
+    "LK/Quantifiers"
+    "LK/Hard_Quantifiers"
+    "LK/Nat"
 
-    Examples for Classical Logic.
-  *}
-  options [document = false]
-  theories
-    Propositional
-    Quantifiers
-    Hard_Quantifiers
-    Nat
-