author  blanchet 
Mon, 26 Nov 2012 13:35:05 +0100  
changeset 50222  40e3c3be6bca 
parent 48738  f8c1a5b9488f 
child 51397  03b586ee5930 
permissions  rwrr 
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48483
diff
changeset

1 
session Sequents = Pure + 
48475  2 
description {* 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1991 University of Cambridge 

5 

6 
Classical Sequent Calculus based on Pure Isabelle. 

7 
*} 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

8 
options [document = false] 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

9 
theories 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

10 
LK 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

11 
ILL 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

12 
ILL_predlog 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

13 
Washing 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

14 
Modal0 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

15 
T 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

16 
S4 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

17 
S43 
48475  18 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48483
diff
changeset

19 
session "SequentsLK" in LK = Sequents + 
48475  20 
description {* 
21 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

22 
Copyright 1992 University of Cambridge 

23 

24 
Examples for Classical Logic. 

25 
*} 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

26 
options [document = false] 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

27 
theories 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

28 
Propositional 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

29 
Quantifiers 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

30 
Hard_Quantifiers 
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset

31 
Nat 
48475  32 