author | nipkow |
Tue, 28 Apr 2020 22:55:51 +0200 | |
changeset 71811 | fa4f8f3d69f2 |
parent 70917 | 693e811b91bb |
child 71924 | e5df9c8d9d4b |
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 |
" |
|
70917
693e811b91bb
more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;
wenzelm
parents:
70914
diff
changeset
|
7 |
options [threads = 1, export_proofs, export_standard_proofs, prune_proofs = false] |
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 |