--- a/src/HOL/Tools/arith_data.ML Fri Mar 13 19:17:57 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML Fri Mar 13 19:17:57 2009 +0100
@@ -10,6 +10,8 @@
val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
val simp_all_tac: thm list -> simpset -> tactic
+ val simplify_meta_eq: thm list -> simpset -> thm -> thm
+ val trans_tac: thm option -> tactic
val prep_simproc: string * string list * (theory -> simpset -> term -> thm option)
-> simproc
end;
@@ -33,6 +35,13 @@
let val ss0 = HOL_ss addsimps rules
in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
+fun simplify_meta_eq rules =
+ let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
+ in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
+
+fun trans_tac NONE = all_tac
+ | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
+
fun prep_simproc (name, pats, proc) = (*FIXME avoid the_context*)
Simplifier.simproc (the_context ()) name pats proc;