changeset 69605 | a96320074298 |
parent 67319 | 07176d5b81d5 |
69604:d80b2df54d31 | 69605:a96320074298 |
---|---|
6 |
6 |
7 theory Realizers |
7 theory Realizers |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 ML_file "~~/src/HOL/Tools/datatype_realizer.ML" |
11 ML_file \<open>~~/src/HOL/Tools/datatype_realizer.ML\<close> |
12 ML_file "~~/src/HOL/Tools/inductive_realizer.ML" |
12 ML_file \<open>~~/src/HOL/Tools/inductive_realizer.ML\<close> |
13 |
13 |
14 end |
14 end |