src/Pure/ROOT1.ML
author wenzelm
Sat, 09 Apr 2016 19:09:11 +0200
changeset 62931 09b516854210
parent 62902 3c0f53eae166
permissions -rw-r--r--
flags as in 'ML' command;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62883
b04e9fe29223 clarified ML bootstrap;
wenzelm
parents:
diff changeset
     1
(*** Isabelle/Pure bootstrap: final setup ***)
b04e9fe29223 clarified ML bootstrap;
wenzelm
parents:
diff changeset
     2
b04e9fe29223 clarified ML bootstrap;
wenzelm
parents:
diff changeset
     3
use_thy "Pure";
62887
6b2c60ebd915 clarified ML bootstrap environment;
wenzelm
parents: 62886
diff changeset
     4
use_thy "ML_Bootstrap";
62883
b04e9fe29223 clarified ML bootstrap;
wenzelm
parents:
diff changeset
     5
62902
3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents: 62887
diff changeset
     6
ML_file "ML/ml_pervasive1.ML";