author | wenzelm |
Sat, 19 Oct 2019 11:29:39 +0200 | |
changeset 70906 | b9567a9f44a0 |
parent 70905 | a6304b4664b6 |
child 70914 | 05c4c6a99b3f |
permissions | -rw-r--r-- |
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
50911
diff
changeset
|
1 |
chapter Pure |
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
50911
diff
changeset
|
2 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48732
diff
changeset
|
3 |
session Pure = |
69319 | 4 |
description " |
5 |
The Pure logical framework. |
|
6 |
" |
|
70906
b9567a9f44a0
proper export of bootstrap proofs (amending a6304b4664b6);
wenzelm
parents:
70905
diff
changeset
|
7 |
options [threads = 1, export_proofs] |
b9567a9f44a0
proper export of bootstrap proofs (amending a6304b4664b6);
wenzelm
parents:
70905
diff
changeset
|
8 |
theories [export_theory] |
70905
a6304b4664b6
more robust -- avoid interference with Proofterm.proofs := 0 in ML_Bootstrap.thy;
wenzelm
parents:
70606
diff
changeset
|
9 |
Pure (global) |
62868
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
62866
diff
changeset
|
10 |
theories |
65473 | 11 |
ML_Bootstrap (global) |
67215 | 12 |
Sessions |