--- 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))"
--- 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
--- 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 | "
--- 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"
--- 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
-