| changeset 67105 | 05ff3e6dbbce |
| parent 64331 | abf7b6e6865f |
| child 67147 | dea94b1aabc3 |
| 67104:a2fa0c6a7aff | 67105:05ff3e6dbbce |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 theory ML_Bootstrap |
7 theory ML_Bootstrap |
8 imports Pure |
8 imports Pure |
9 begin |
9 begin |
10 |
|
11 external_file "$POLYML_EXE" |
|
12 |
|
10 |
13 |
11 subsection \<open>Standard ML environment for virtual bootstrap\<close> |
14 subsection \<open>Standard ML environment for virtual bootstrap\<close> |
12 |
15 |
13 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
16 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close> |
14 |
17 |