author | wenzelm |
Sun, 20 Oct 2019 16:16:23 +0200 | |
changeset 70914 | 05c4c6a99b3f |
parent 70906 | b9567a9f44a0 |
child 70917 | 693e811b91bb |
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 |
" |
|
70914
05c4c6a99b3f
option to export standardized proof terms (not scalable);
wenzelm
parents:
70906
diff
changeset
|
7 |
options [threads = 1, export_proofs, export_standard_proofs] |
70906
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 |