author | wenzelm |
Mon, 01 Oct 2012 20:17:30 +0200 | |
changeset 49677 | c4e2762a265c |
parent 48738 | f8c1a5b9488f |
child 51397 | 03b586ee5930 |
permissions | -rw-r--r-- |
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 "Sequents-LK" 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 |