equal
deleted
inserted
replaced
7 theory ML_Bootstrap |
7 theory ML_Bootstrap |
8 imports Pure |
8 imports Pure |
9 begin |
9 begin |
10 |
10 |
11 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
11 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
12 SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close> |
12 |
|
13 SML_import \<open> |
|
14 structure Output_Primitives = Output_Primitives_Virtual; |
|
15 structure Thread_Data = Thread_Data_Virtual; |
|
16 \<close> |
|
17 |
13 setup \<open>Config.put_global ML_Env.SML_environment true\<close> |
18 setup \<open>Config.put_global ML_Env.SML_environment true\<close> |
14 |
19 |
15 end |
20 end |