simplified sessions;
authorwenzelm
Sat Feb 01 18:00:28 2014 +0100 (2014-02-01)
changeset 5522908f2ebb65078
parent 55228 901a6696cdd8
child 55230 cb5ef74b32f9
simplified sessions;
src/Sequents/LK/Hard_Quantifiers.thy
src/Sequents/LK/Nat.thy
src/Sequents/LK/Propositional.thy
src/Sequents/LK/Quantifiers.thy
src/Sequents/ROOT
     1.1 --- a/src/Sequents/LK/Hard_Quantifiers.thy	Sat Feb 01 17:56:03 2014 +0100
     1.2 +++ b/src/Sequents/LK/Hard_Quantifiers.thy	Sat Feb 01 18:00:28 2014 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  *)
     1.5  
     1.6  theory Hard_Quantifiers
     1.7 -imports LK
     1.8 +imports "../LK"
     1.9  begin
    1.10  
    1.11  lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
     2.1 --- a/src/Sequents/LK/Nat.thy	Sat Feb 01 17:56:03 2014 +0100
     2.2 +++ b/src/Sequents/LK/Nat.thy	Sat Feb 01 18:00:28 2014 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
     2.5  
     2.6  theory Nat
     2.7 -imports LK
     2.8 +imports "../LK"
     2.9  begin
    2.10  
    2.11  typedecl nat
     3.1 --- a/src/Sequents/LK/Propositional.thy	Sat Feb 01 17:56:03 2014 +0100
     3.2 +++ b/src/Sequents/LK/Propositional.thy	Sat Feb 01 18:00:28 2014 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Classical sequent calculus: examples with propositional connectives *}
     3.5  
     3.6  theory Propositional
     3.7 -imports LK
     3.8 +imports "../LK"
     3.9  begin
    3.10  
    3.11  text "absorptive laws of & and | "
     4.1 --- a/src/Sequents/LK/Quantifiers.thy	Sat Feb 01 17:56:03 2014 +0100
     4.2 +++ b/src/Sequents/LK/Quantifiers.thy	Sat Feb 01 18:00:28 2014 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  *)
     4.5  
     4.6  theory Quantifiers
     4.7 -imports LK
     4.8 +imports "../LK"
     4.9  begin
    4.10  
    4.11  lemma "|- (ALL x. P)  <->  P"
     5.1 --- a/src/Sequents/ROOT	Sat Feb 01 17:56:03 2014 +0100
     5.2 +++ b/src/Sequents/ROOT	Sat Feb 01 18:00:28 2014 +0100
     5.3 @@ -48,17 +48,9 @@
     5.4      S4
     5.5      S43
     5.6  
     5.7 -session "Sequents-LK" in LK = Sequents +
     5.8 -  description {*
     5.9 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    5.10 -    Copyright   1992  University of Cambridge
    5.11 +    (* Examples for Classical Logic *)
    5.12 +    "LK/Propositional"
    5.13 +    "LK/Quantifiers"
    5.14 +    "LK/Hard_Quantifiers"
    5.15 +    "LK/Nat"
    5.16  
    5.17 -    Examples for Classical Logic.
    5.18 -  *}
    5.19 -  options [document = false]
    5.20 -  theories
    5.21 -    Propositional
    5.22 -    Quantifiers
    5.23 -    Hard_Quantifiers
    5.24 -    Nat
    5.25 -