equal
deleted
inserted
replaced
5 |
5 |
6 header {* Generic reflection and reification *} |
6 header {* Generic reflection and reification *} |
7 |
7 |
8 theory Reflection |
8 theory Reflection |
9 imports Main |
9 imports Main |
10 uses "reflection.ML" |
10 uses ("reflection.ML") |
11 begin |
11 begin |
|
12 |
|
13 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g" |
|
14 by (blast intro: ext) |
|
15 use "reflection.ML" |
12 |
16 |
13 method_setup reify = {* |
17 method_setup reify = {* |
14 fn src => |
18 fn src => |
15 Method.syntax (Attrib.thms -- |
19 Method.syntax (Attrib.thms -- |
16 Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #> |
20 Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #> |