author | wenzelm |
Thu, 07 Apr 2016 21:27:17 +0200 | |
changeset 62910 | f37878ebba65 |
parent 62902 | 3c0f53eae166 |
child 62923 | 3a122e1e352a |
permissions | -rw-r--r-- |
62883 | 1 |
(*** Isabelle/Pure bootstrap: initial setup ***) |
2 |
||
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62890
diff
changeset
|
3 |
ML_file "Concurrent/thread_data.ML"; |
62910
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
62902
diff
changeset
|
4 |
ML_file "ML/ml_recursive.ML" |