equal
deleted
inserted
replaced
4 |
4 |
5 header {* Generic reflection and reification *} |
5 header {* Generic reflection and reification *} |
6 |
6 |
7 theory Reflection |
7 theory Reflection |
8 imports Main |
8 imports Main |
9 uses |
|
10 "~~/src/HOL/Library/reify_data.ML" |
|
11 "~~/src/HOL/Library/reflection.ML" |
|
12 begin |
9 begin |
|
10 |
|
11 ML_file "~~/src/HOL/Library/reify_data.ML" |
|
12 ML_file "~~/src/HOL/Library/reflection.ML" |
13 |
13 |
14 setup {* Reify_Data.setup *} |
14 setup {* Reify_Data.setup *} |
15 |
15 |
16 method_setup reify = {* |
16 method_setup reify = {* |
17 Attrib.thms -- |
17 Attrib.thms -- |