isabelle: src/HOL/ex/Reflection.thy@a3efbae45735

     1 (*

     2     ID:         $Id$

     3     Author:     Amine Chaieb, TU Muenchen

     4 *)

     6 header {* Generic reflection and reification *}

     8 theory Reflection

     9 imports Main

    10 uses ("reflection.ML")

    11 begin

    13 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"

    14   by (blast intro: ext)

    15 use "reflection.ML"

    17 method_setup reify = {*

    18   fn src =>

    19     Method.syntax (Attrib.thms --

    20       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>

    21   (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))

    22 *} "partial automatic reification"

    24 method_setup reflection = {*

    25   fn src =>

    26     Method.syntax (Attrib.thms --

    27       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>

    28   (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))

    29 *} "reflection method"

    31 end

author	haftmann
	Mon Dec 18 08:21:35 2006 +0100 (2006-12-18)
changeset 21879	a3efbae45735
parent 21588	cd0dc678a205
child 22199	b617ddd200eb
permissions	-rw-r--r--