equal
deleted
inserted
replaced
|
1 (* |
|
2 ID: $Id$ |
|
3 Author: Amine Chaieb, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Generic reflection and reification *} |
|
7 |
|
8 theory Reflection |
|
9 imports Main |
|
10 uses "reflection.ML" |
|
11 begin |
|
12 |
|
13 method_setup reify = {* |
|
14 fn src => |
|
15 Method.syntax (Attrib.thms -- |
|
16 Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #> |
|
17 (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.genreify_tac ctxt eqs to)) |
|
18 *} "partial automatic reification" |
|
19 |
|
20 method_setup reflection = {* |
|
21 fn src => |
|
22 Method.syntax (Attrib.thms -- |
|
23 Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #> |
|
24 (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.reflection_tac ctxt ths to)) |
|
25 *} "reflection method" |
|
26 |
|
27 end |