| author | wenzelm |
| Tue, 21 Apr 2020 19:07:49 +0200 | |
| changeset 71775 | 291c46bf3000 |
| 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 |