# HG changeset patch # User wenzelm # Date 1329430021 -3600 # Node ID 696f3fec3f836218fa1fa0313069311af1f867bb # Parent c4b2ec379fdd448b5f91eb7ff156075094b6b5fd more antiquotations; diff -r c4b2ec379fdd -r 696f3fec3f83 src/HOL/Library/Reflection.thy --- a/src/HOL/Library/Reflection.thy Thu Feb 16 22:54:40 2012 +0100 +++ b/src/HOL/Library/Reflection.thy Thu Feb 16 23:07:01 2012 +0100 @@ -11,9 +11,6 @@ setup {* Reify_Data.setup *} -lemma ext2: "(\x. f x = g x) \ f = g" - by blast - use "reflection.ML" method_setup reify = {* diff -r c4b2ec379fdd -r 696f3fec3f83 src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Thu Feb 16 22:54:40 2012 +0100 +++ b/src/HOL/Library/reflection.ML Thu Feb 16 23:07:01 2012 +0100 @@ -16,10 +16,6 @@ structure Reflection : REFLECTION = struct -val ext2 = @{thm ext2}; -val nth_Cons_0 = @{thm nth_Cons_0}; -val nth_Cons_Suc = @{thm nth_Cons_Suc}; - (* Make a congruence rule out of a defining equation for the interpretation *) (* th is one defining equation of f, i.e. th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *) @@ -59,7 +55,7 @@ fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t))) | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t)) - fun tryext x = (x RS ext2 handle THM _ => x) + fun tryext x = (x RS @{lemma "(\x. f x = g x) \ f = g" by blast} handle THM _ => x) val cong = (Goal.prove ctxt'' [] (map mk_def env) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs))) @@ -295,7 +291,8 @@ val th = trytrans corr_thms val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th val rth = conv ft - in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc]) + in + simplify (HOL_basic_ss addsimps raw_eqs addsimps @{thms nth_Cons_0 nth_Cons_Suc}) (simplify (HOL_basic_ss addsimps [rth]) th) end