| author | wenzelm |
| Thu Aug 03 15:03:05 2006 +0200 (2006-08-03) | |
| changeset 20319 | a8761e8568de |
| child 20374 | 01b711328990 |
| permissions | -rw-r--r-- |
| wenzelm@20319 | 1 |
(* |
| wenzelm@20319 | 2 |
ID: $Id$ |
| wenzelm@20319 | 3 |
Author: Amine Chaieb, TU Muenchen |
| wenzelm@20319 | 4 |
*) |
| wenzelm@20319 | 5 |
|
| wenzelm@20319 | 6 |
header {* Generic reflection and reification *}
|
| wenzelm@20319 | 7 |
|
| wenzelm@20319 | 8 |
theory Reflection |
| wenzelm@20319 | 9 |
imports Main |
| wenzelm@20319 | 10 |
uses "reflection.ML" |
| wenzelm@20319 | 11 |
begin |
| wenzelm@20319 | 12 |
|
| wenzelm@20319 | 13 |
method_setup reify = {*
|
| wenzelm@20319 | 14 |
fn src => |
| wenzelm@20319 | 15 |
Method.syntax (Attrib.thms -- |
| wenzelm@20319 | 16 |
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
|
| wenzelm@20319 | 17 |
(fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.genreify_tac ctxt eqs to)) |
| wenzelm@20319 | 18 |
*} "partial automatic reification" |
| wenzelm@20319 | 19 |
|
| wenzelm@20319 | 20 |
method_setup reflection = {*
|
| wenzelm@20319 | 21 |
fn src => |
| wenzelm@20319 | 22 |
Method.syntax (Attrib.thms -- |
| wenzelm@20319 | 23 |
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
|
| wenzelm@20319 | 24 |
(fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.reflection_tac ctxt ths to)) |
| wenzelm@20319 | 25 |
*} "reflection method" |
| wenzelm@20319 | 26 |
|
| wenzelm@20319 | 27 |
end |