| author | wenzelm | 
| Mon, 09 Mar 2020 14:30:09 +0100 | |
| changeset 71529 | dd56597e026b | 
| parent 70917 | 693e811b91bb | 
| child 71924 | e5df9c8d9d4b | 
| permissions | -rw-r--r-- | 
| 51397 
03b586ee5930
support for 'chapter' specifications within session ROOT;
 wenzelm parents: 
50911diff
changeset | 1 | chapter Pure | 
| 
03b586ee5930
support for 'chapter' specifications within session ROOT;
 wenzelm parents: 
50911diff
changeset | 2 | |
| 48738 
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
 wenzelm parents: 
48732diff
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: 
70914diff
changeset | 7 | options [threads = 1, export_proofs, export_standard_proofs, prune_proofs = false] | 
| 70906 
b9567a9f44a0
proper export of bootstrap proofs (amending a6304b4664b6);
 wenzelm parents: 
70905diff
changeset | 8 | theories [export_theory] | 
| 70905 
a6304b4664b6
more robust -- avoid interference with Proofterm.proofs := 0 in ML_Bootstrap.thy;
 wenzelm parents: 
70606diff
changeset | 9 | Pure (global) | 
| 62868 
61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;
 wenzelm parents: 
62866diff
changeset | 10 | theories | 
| 65473 | 11 | ML_Bootstrap (global) | 
| 67215 | 12 | Sessions |