src/Pure/ROOT
author immler
Sun, 03 Nov 2019 21:46:46 -0500
changeset 71034 e0755162093f
parent 70917 693e811b91bb
child 71924 e5df9c8d9d4b
permissions -rw-r--r--
replace approximation oracle by less ad-hoc @{computation}s
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
     4
  description "
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
     5
    The Pure logical framework.
baccaf89ca0d tuned -- refining auto-update 15e9ed5b28fb;
wenzelm
parents: 69272
diff changeset
     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
b47373f52451 more global theories;
wenzelm
parents: 65374
diff changeset
    11
    ML_Bootstrap (global)
67215
03d0c958d65a PIDE markup for session ROOT files;
wenzelm
parents: 65473
diff changeset
    12
    Sessions