src/Pure/ROOT1.ML
author wenzelm
Wed, 06 Apr 2016 14:02:12 +0200
changeset 62887 6b2c60ebd915
parent 62886 72c475e03e22
child 62902 3c0f53eae166
permissions -rw-r--r--
clarified ML bootstrap environment;
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
b04e9fe29223 clarified ML bootstrap;
wenzelm
parents:
diff changeset
     6
use "ML/ml_pervasive1.ML";