src/Pure/ML_Bootstrap.thy
author wenzelm
Sat Apr 09 16:16:05 2016 +0200 (2016-04-09)
changeset 62930 51ac6bc389e8
parent 62902 3c0f53eae166
child 62944 3ee643c5ed00
permissions -rw-r--r--
shared output primitives of physical/virtual Pure;
     1 (*  Title:      Pure/ML_Bootstrap.thy
     2     Author:     Makarius
     3 
     4 ML bootstrap environment -- with access to low-level structures!
     5 *)
     6 
     7 theory ML_Bootstrap
     8 imports Pure
     9 begin
    10 
    11 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
    12 
    13 SML_import \<open>
    14 structure Output_Primitives = Output_Primitives_Virtual;
    15 structure Thread_Data = Thread_Data_Virtual;
    16 \<close>
    17 
    18 setup \<open>Config.put_global ML_Env.SML_environment true\<close>
    19 
    20 end