author | wenzelm |
Fri, 10 Sep 2021 21:55:55 +0200 | |
changeset 74286 | 641300b56ebe |
parent 71924 | e5df9c8d9d4b |
child 74287 | f79dfc7656ae |
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 |
71924
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
70917
diff
changeset
|
13 |
|
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
70917
diff
changeset
|
14 |
session "Pure-Examples" in Examples = Pure + |
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
70917
diff
changeset
|
15 |
description " |
74286 | 16 |
Notable Examples for Isabelle/Pure. |
71924
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
70917
diff
changeset
|
17 |
" |
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
70917
diff
changeset
|
18 |
theories |
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
70917
diff
changeset
|
19 |
First_Order_Logic |
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
70917
diff
changeset
|
20 |
Higher_Order_Logic |
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
70917
diff
changeset
|
21 |
document_files |
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
70917
diff
changeset
|
22 |
"root.bib" |
e5df9c8d9d4b
clarified sessions: "Notable Examples in Isabelle/Pure";
wenzelm
parents:
70917
diff
changeset
|
23 |
"root.tex" |