changeset 62881 | 20b0cb2f0b87 |
parent 62880 | 76e7d9169b54 |
child 62883 | b04e9fe29223 |
62880:76e7d9169b54 | 62881:20b0cb2f0b87 |
---|---|
5 *) |
5 *) |
6 |
6 |
7 theory ML_Root |
7 theory ML_Root |
8 imports Pure |
8 imports Pure |
9 keywords "use" "use_debug" "use_no_debug" :: thy_load |
9 keywords "use" "use_debug" "use_no_debug" :: thy_load |
10 and "use_thy" :: thy_load |
10 and "use_thy" :: thy_load ("thy") |
11 begin |
11 begin |
12 |
12 |
13 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
13 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
14 |
14 |
15 ML \<open> |
15 ML \<open> |