| changeset 45966 | 03ce2b2a29a2 |
| parent 42814 | 5af15f1e2ef6 |
| child 46510 | 696f3fec3f83 |
| 45965:2af982715e5c | 45966:03ce2b2a29a2 |
|---|---|
10 begin |
10 begin |
11 |
11 |
12 setup {* Reify_Data.setup *} |
12 setup {* Reify_Data.setup *} |
13 |
13 |
14 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g" |
14 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g" |
15 by (blast intro: ext) |
15 by blast |
16 |
16 |
17 use "reflection.ML" |
17 use "reflection.ML" |
18 |
18 |
19 method_setup reify = {* |
19 method_setup reify = {* |
20 Attrib.thms -- |
20 Attrib.thms -- |