--- a/src/HOL/Tools/BNF/bnf_tactics.ML Fri Sep 12 17:51:31 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML Sat Sep 13 18:08:38 2014 +0200
@@ -11,6 +11,7 @@
include CTR_SUGAR_GENERAL_TACTICS
val fo_rtac: thm -> Proof.context -> int -> tactic
+ val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
int -> tactic
@@ -41,6 +42,9 @@
end
handle Pattern.MATCH => no_tac);
+(*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*)
+fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
+
(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
fun mk_pointfree ctxt thm = thm
|> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq