--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Jul 24 22:20:22 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Fri Jul 24 22:29:06 2015 +0200
@@ -212,7 +212,7 @@
EVERY' [rtac ctxt sym, rtac ctxt trans, rtac ctxt (refl RSN (2, @{thm SUP_cong})),
etac ctxt (morE RS sym RS arg_cong RS trans), assume_tac ctxt, rtac ctxt set_map0,
rtac ctxt (@{thm UN_simps(10)} RS trans), rtac ctxt (refl RS @{thm SUP_cong}),
- ftac ctxt coalg_set, assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt,
+ forward_tac ctxt [coalg_set], assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt,
rtac ctxt mp, rtac ctxt (mk_conjunctN n i),
REPEAT_DETERM o etac ctxt allE, assume_tac ctxt, assume_tac ctxt])
(rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
@@ -418,7 +418,7 @@
end;
fun mk_length_Lev'_tac ctxt length_Lev =
- EVERY' [ftac ctxt length_Lev, etac ctxt ssubst, assume_tac ctxt] 1;
+ EVERY' [forward_tac ctxt [length_Lev], etac ctxt ssubst, assume_tac ctxt] 1;
fun mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss =
let
@@ -720,7 +720,7 @@
let
val n = length Rep_injects;
in
- EVERY' [rtac ctxt rev_mp, ftac ctxt (bis_def RS iffD1),
+ EVERY' [rtac ctxt rev_mp, forward_tac ctxt [bis_def RS iffD1],
REPEAT_DETERM o etac ctxt conjE, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_converse,
rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, assume_tac ctxt,
rtac ctxt bis_Gr, rtac ctxt tcoalg,
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Fri Jul 24 22:20:22 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Fri Jul 24 22:29:06 2015 +0200
@@ -340,7 +340,8 @@
CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
fun alg_epi_tac ((alg_set, str_init_def), set_map) =
EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
- rtac ctxt ballI, ftac ctxt (alg_select RS bspec), rtac ctxt (str_init_def RS @{thm ssubst_mem}),
+ rtac ctxt ballI, forward_tac ctxt [alg_select RS bspec],
+ rtac ctxt (str_init_def RS @{thm ssubst_mem}),
etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map,
rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
assume_tac ctxt]];
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Jul 24 22:20:22 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Jul 24 22:29:06 2015 +0200
@@ -57,7 +57,6 @@
val rtac: Proof.context -> thm -> int -> tactic
val etac: Proof.context -> thm -> int -> tactic
val dtac: Proof.context -> thm -> int -> tactic
- val ftac: Proof.context -> thm -> int -> tactic
val list_all_free: term list -> term -> term
val list_exists_free: term list -> term -> term
@@ -281,6 +280,5 @@
fun rtac ctxt thm = resolve_tac ctxt [thm];
fun etac ctxt thm = eresolve_tac ctxt [thm];
fun dtac ctxt thm = dresolve_tac ctxt [thm];
-fun ftac ctxt thm = forward_tac ctxt [thm];
end;