author  wenzelm 
Tue, 24 Jul 2012 20:42:34 +0200  
changeset 48483  9bfb6978eb80 
parent 48475  02dd825f5a4e 
child 48738  f8c1a5b9488f 
permissions  rwrr 
48475  1 
session Sequents! in "." = Pure + 
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 

19 
session LK = Sequents + 

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 