author | wenzelm |
Mon, 11 Mar 2013 13:28:46 +0100 | |
changeset 51397 | 03b586ee5930 |
parent 48738 | f8c1a5b9488f |
child 51403 | 2ff3a5589b05 |
permissions | -rw-r--r-- |
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
48738
diff
changeset
|
1 |
chapter LCF |
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
48738
diff
changeset
|
2 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48483
diff
changeset
|
3 |
session LCF = Pure + |
48475 | 4 |
description {* |
5 |
Author: Tobias Nipkow |
|
6 |
Copyright 1992 University of Cambridge |
|
7 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset
|
8 |
options [document = false] |
48475 | 9 |
theories LCF |
10 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48483
diff
changeset
|
11 |
session "LCF-ex" in ex = LCF + |
48475 | 12 |
description {* |
13 |
Author: Tobias Nipkow |
|
14 |
Copyright 1991 University of Cambridge |
|
15 |
||
16 |
Some examples from Lawrence Paulson's book Logic and Computation. |
|
17 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset
|
18 |
options [document = false] |
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset
|
19 |
theories |
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset
|
20 |
Ex1 |
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset
|
21 |
Ex2 |
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset
|
22 |
Ex3 |
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48475
diff
changeset
|
23 |
Ex4 |
48475 | 24 |