tuned tactics

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Mar 13 11:15:04 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Mar 13 16:28:25 2014 +0100
@@ -348,7 +348,7 @@
           (HOLogic.mk_Trueprop (mk_tcoalg activeAs ss))
       in
         Goal.prove_sorry lthy [] [] goal
-          (K (stac coalg_def 1 THEN CONJ_WRAP
+          (K (rtac (coalg_def RS iffD2) 1 THEN CONJ_WRAP
             (K (EVERY' [rtac ballI, rtac CollectI,
               CONJ_WRAP' (K (EVERY' [rtac @{thm subset_UNIV}])) allAs] 1)) ss))
         |> Thm.close_derivation

--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Mar 13 11:15:04 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Mar 13 16:28:25 2014 +0100
@@ -117,27 +117,29 @@
   REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1;
 
 fun mk_mor_elim_tac mor_def =
-  (dtac (subst OF [mor_def]) THEN'
+  (dtac (mor_def RS iffD1) THEN'
   REPEAT o etac conjE THEN'
   TRY o rtac @{thm image_subsetI} THEN'
   etac bspec THEN'
   atac) 1;
 
 fun mk_mor_incl_tac mor_def map_ids =
-  (stac mor_def THEN'
+  (rtac (mor_def RS iffD2) THEN'
   rtac conjI THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN'
+  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, etac (id_apply RS @{thm ssubst_mem})]))
+    map_ids THEN'
   CONJ_WRAP' (fn thm =>
-   (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_ids) 1;
+    (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_ids) 1;
 
 fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
   let
-    fun fbetw_tac image = EVERY' [rtac ballI, stac o_apply, etac image, etac image, atac];
+    fun fbetw_tac image = EVERY' [rtac ballI, rtac (o_apply RS @{thm ssubst_mem}), etac image,
+      etac image, atac];
     fun mor_tac ((mor_image, morE), map_comp_id) =
       EVERY' [rtac ballI, stac o_apply, rtac trans, rtac (map_comp_id RS sym), rtac trans,
         etac (morE RS arg_cong), atac, etac morE, etac mor_image, atac];
   in
-    (stac mor_def THEN' rtac conjI THEN'
+    (rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
     CONJ_WRAP' fbetw_tac mor_images THEN'
     CONJ_WRAP' mor_tac ((mor_images ~~ morEs) ~~ map_comp_ids)) 1
   end;
@@ -149,16 +151,16 @@
       rtac UNIV_I, rtac sym, rtac o_apply];
   in
     EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
-    stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
+    rtac (mor_def RS iffD2), rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
     CONJ_WRAP' (fn i =>
       EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm comp_eq_dest}]) (1 upto n)] 1
   end;
 
 fun mk_mor_str_tac ks mor_UNIV =
-  (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac refl)) ks) 1;
+  (rtac (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac refl)) ks) 1;
 
 fun mk_mor_case_sum_tac ks mor_UNIV =
-  (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1;
+  (rtac (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1;
 
 fun mk_set_incl_hset_tac rec_Suc =
   EVERY' (map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym,
@@ -262,7 +264,7 @@
   end;
 
 fun mk_bis_converse_tac m bis_rel rel_congs rel_converseps =
-  EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
+  EVERY' [rtac (bis_rel RS iffD2), dtac (bis_rel RS iffD1),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [rtac converse_shift, etac subset_trans,
       rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
@@ -276,7 +278,7 @@
         rtac @{thm conversepI}, etac mp, etac @{thm converseD}]) (rel_congs ~~ rel_converseps)] 1;
 
 fun mk_bis_O_tac ctxt m bis_rel rel_congs rel_OOs =
-  EVERY' [stac bis_rel, REPEAT_DETERM o dtac (bis_rel RS iffD1),
+  EVERY' [rtac (bis_rel RS iffD2), REPEAT_DETERM o dtac (bis_rel RS iffD1),
     REPEAT_DETERM o etac conjE, rtac conjI,
     CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) rel_congs,
     CONJ_WRAP' (fn (rel_cong, rel_OO) =>
@@ -294,7 +296,7 @@
 fun mk_bis_Gr_tac ctxt bis_rel rel_Grps mor_images morEs coalg_ins =
   unfold_thms_tac ctxt (bis_rel :: @{thm eq_alt} :: @{thm in_rel_Gr} :: rel_Grps) THEN
   EVERY' [rtac conjI,
-    CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
+    CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS iffD2) THEN' etac thm) mor_images,
     CONJ_WRAP' (fn (coalg_in, morE) =>
       EVERY' [rtac allI, rtac allI, rtac impI, rtac @{thm GrpI}, etac (morE RS trans),
         etac @{thm GrD1}, etac (@{thm GrD2} RS arg_cong), etac coalg_in, etac @{thm GrD1}])
@@ -560,7 +562,7 @@
             (set_Levs, set_image_Levs))))) =>
             EVERY' [rtac ballI,
               REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
-              rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst),
+              rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS iffD2),
               rtac exI, rtac conjI,
               if n = 1 then rtac refl
               else etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i),
@@ -578,7 +580,7 @@
           (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
             (set_Levss ~~ set_image_Levss))))),
         (*root isNode*)
-          rtac (isNode_def RS ssubst), rtac exI, rtac conjI,
+          rtac (isNode_def RS iffD2), rtac exI, rtac conjI,
           CONVERSION (Conv.top_conv
             (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
           if n = 1 then rtac refl else rtac (mk_sum_caseN n i),
@@ -622,7 +624,7 @@
             rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
             rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
             REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac,
-            rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI,
+            rtac trans, rtac @{thm shift_def}, rtac iffD2, rtac @{thm fun_eq_iff}, rtac allI,
             CONVERSION (Conv.top_conv
               (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
             if n = 1 then K all_tac
@@ -632,7 +634,7 @@
   in
     (rtac mor_cong THEN'
     EVERY' (map (fn thm => rtac (thm RS @{thm ext})) beh_defs) THEN'
-    stac mor_def THEN' rtac conjI THEN'
+    rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
     CONJ_WRAP' fbetw_tac
       (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~
         (rv_lastss ~~ (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))) THEN'
@@ -653,22 +655,22 @@
     etac (sym RS arg_cong RS trans), rtac map_comp_id] 1;
 
 fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss =
-  EVERY' [stac coalg_def,
+  EVERY' [rtac (coalg_def RS iffD2),
     CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
       EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
         rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
         REPEAT_DETERM_N m o EVERY' [rtac conjI, rtac subset_UNIV],
         CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
           EVERY' [rtac (set_map0 RS ord_eq_le_trans),
-            rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
+            rtac @{thm image_subsetI}, rtac iffD2, rtac @{thm proj_in_iff},
             rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
         (equiv_LSBISs ~~ (drop m set_map0s ~~ coalgT_sets))])
     ((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
 
 fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
-  EVERY' [stac mor_def, rtac conjI,
+  EVERY' [rtac (mor_def RS iffD2), rtac conjI,
     CONJ_WRAP' (fn equiv_LSBIS =>
-      EVERY' [rtac ballI, rtac ssubst, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, atac])
+      EVERY' [rtac ballI, rtac iffD2, rtac @{thm proj_in_iff}, rtac equiv_LSBIS, atac])
     equiv_LSBISs,
     CONJ_WRAP' (fn (equiv_LSBIS, congruent_str_final) =>
       EVERY' [rtac ballI, rtac sym, rtac trans, rtac @{thm univ_commute}, rtac equiv_LSBIS,
@@ -754,7 +756,7 @@
   etac unfold_unique_mor 1;
 
 fun mk_dtor_coinduct_tac m raw_coind bis_rel rel_congs =
-  EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_rel, rtac conjI,
+  EVERY' [rtac rev_mp, rtac raw_coind, rtac iffD2, rtac bis_rel, rtac conjI,
     CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]}))
     rel_congs,
     CONJ_WRAP' (fn rel_cong => EVERY' [rtac allI, rtac allI, rtac impI,

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Mar 13 11:15:04 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Mar 13 16:28:25 2014 +0100
@@ -296,7 +296,7 @@
           (HOLogic.mk_Trueprop (mk_talg activeAs ss))
       in
         Goal.prove_sorry lthy [] [] goal
-          (K (stac alg_def 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
+          (K (rtac (alg_def RS iffD2) 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
         |> Thm.close_derivation
       end;
 
@@ -985,7 +985,7 @@
       lthy
       |> fold_map3 (fn b => fn mx => fn car_init =>
         typedef (Binding.conceal b, params, mx) car_init NONE
-          (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
+          (EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
             rtac alg_init_thm] 1)) bs mixfixes car_inits
       |>> apsnd split_list o split_list;
 
@@ -1005,7 +1005,7 @@
     fun mk_inver_thm mk_tac rep abs X thm =
       Goal.prove_sorry lthy [] []
         (HOLogic.mk_Trueprop (mk_inver rep abs X))
-        (K (EVERY' [rtac ssubst, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1))
+        (K (EVERY' [rtac iffD2, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1))
       |> Thm.close_derivation;
 
     val inver_Reps = map4 (mk_inver_thm rtac) Abs_Ts Rep_Ts (map HOLogic.mk_UNIV Ts) Rep_inverses;

--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Mar 13 11:15:04 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Mar 13 16:28:25 2014 +0100
@@ -86,7 +86,8 @@
 val subset_trans = @{thm subset_trans};
 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
 val rev_bspec = Drule.rotate_prems 1 bspec;
-val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}
+val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
+val relChainD = @{thm iffD2[OF meta_eq_to_obj_eq[OF relChain_def]]};
 
 fun mk_alg_set_tac alg_def =
   EVERY' [dtac (alg_def RS iffD1), REPEAT_DETERM o etac conjE, etac bspec, rtac CollectI,
@@ -102,24 +103,26 @@
   etac @{thm emptyE}) 1;
 
 fun mk_mor_elim_tac mor_def =
-  (dtac (subst OF [mor_def]) THEN'
+  (dtac (mor_def RS iffD1) THEN'
   REPEAT o etac conjE THEN'
   TRY o rtac @{thm image_subsetI} THEN'
   etac bspec THEN'
   atac) 1;
 
 fun mk_mor_incl_tac mor_def map_ids =
-  (stac mor_def THEN'
+  (rtac (mor_def RS iffD2) THEN'
   rtac conjI THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN'
+  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, etac (id_apply RS @{thm ssubst_mem})]))
+    map_ids THEN'
   CONJ_WRAP' (fn thm =>
-   (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_ids) 1;
+    (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_ids) 1;
 
 fun mk_mor_comp_tac mor_def set_maps map_comp_ids =
   let
-    val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac];
+    val fbetw_tac =
+      EVERY' [rtac ballI, rtac (o_apply RS @{thm ssubst_mem}), etac bspec, etac bspec, atac];
     fun mor_tac (set_map, map_comp_id) =
-      EVERY' [rtac ballI, stac o_apply, rtac trans,
+      EVERY' [rtac ballI, rtac (o_apply RS trans), rtac trans,
         rtac trans, dtac rev_bspec, atac, etac arg_cong,
          REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN'
       CONJ_WRAP' (fn thm =>
@@ -128,7 +131,7 @@
             etac bspec, etac set_mp, atac])]) set_map THEN'
       rtac (map_comp_id RS arg_cong);
   in
-    (dtac (mor_def RS subst) THEN' dtac (mor_def RS subst) THEN' stac mor_def THEN'
+    (dtac (mor_def RS iffD1) THEN' dtac (mor_def RS iffD1) THEN' rtac (mor_def RS iffD2) THEN'
     REPEAT o etac conjE THEN'
     rtac conjI THEN'
     CONJ_WRAP' (K fbetw_tac) set_maps THEN'
@@ -150,9 +153,9 @@
          rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map,
          rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_cong0L RS arg_cong),
          REPEAT_DETERM_N (length morEs) o
-           (EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
+           (EVERY' [rtac iffD1, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
   in
-    (stac mor_def THEN'
+    (rtac (mor_def RS iffD2) THEN'
     dtac (alg_def RS iffD1) THEN'
     dtac (alg_def RS iffD1) THEN'
     REPEAT o etac conjE THEN'
@@ -162,12 +165,12 @@
   end;
 
 fun mk_mor_str_tac ks mor_def =
-  (stac mor_def THEN' rtac conjI THEN'
+  (rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
   CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN'
   CONJ_WRAP' (K (EVERY' [rtac ballI, rtac refl])) ks) 1;
 
 fun mk_mor_convol_tac ks mor_def =
-  (stac mor_def THEN' rtac conjI THEN'
+  (rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
   CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN'
   CONJ_WRAP' (K (EVERY' [rtac ballI, rtac trans, rtac @{thm fst_convol'}, rtac o_apply])) ks) 1;
 
@@ -179,17 +182,17 @@
       rtac sym, rtac o_apply];
   in
     EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs,
-    stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
-    REPEAT_DETERM o etac conjE, REPEAT_DETERM_N n o dtac (@{thm fun_eq_iff} RS subst),
+    rtac (mor_def RS iffD2), rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs,
+    REPEAT_DETERM o etac conjE, REPEAT_DETERM_N n o dtac (@{thm fun_eq_iff} RS iffD1),
     CONJ_WRAP' (K (EVERY' [rtac ballI, REPEAT_DETERM o etac allE, rtac trans,
-      etac (o_apply RS subst), rtac o_apply])) morEs] 1
+      etac (o_apply RS sym RS trans), rtac o_apply])) morEs] 1
   end;
 
 fun mk_iso_alt_tac mor_images mor_inv =
   let
     val n = length mor_images;
     fun if_wrap_tac thm =
-      EVERY' [rtac ssubst, rtac @{thm bij_betw_iff_ex}, rtac exI, rtac conjI,
+      EVERY' [rtac iffD2, rtac @{thm bij_betw_iff_ex}, rtac exI, rtac conjI,
         rtac @{thm inver_surj}, etac thm, etac thm, atac, etac conjI, atac]
     val if_tac =
       EVERY' [etac thin_rl, etac thin_rl, REPEAT o eresolve_tac [conjE, exE],
@@ -222,7 +225,7 @@
       (set_maps ~~ alg_sets);
   in
     (rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN'
-    stac alg_def THEN' copy_str_tac) 1
+    rtac (alg_def RS iffD2) THEN' copy_str_tac) 1
   end;
 
 fun mk_copy_alg_tac ctxt set_maps alg_sets mor_def iso_alt copy_str =
@@ -240,7 +243,7 @@
       (set_maps ~~ alg_sets);
   in
     (rtac (iso_alt RS iffD2) THEN' etac copy_str THEN' REPEAT_DETERM o atac THEN'
-    rtac conjI THEN' stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN'
+    rtac conjI THEN' rtac (mor_def RS iffD2) THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN'
     CONJ_WRAP' (K atac) alg_sets) 1
   end;
 
@@ -270,16 +273,16 @@
       EVERY' [rtac Un_cong, minG_tac, rtac @{thm image_cong}, rtac thm,
         REPEAT_DETERM_N (length in_congs) o minG_tac, rtac refl];
   in
-    (rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ssubst THEN'
+    (rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac iffD2 THEN'
     rtac meta_eq_to_obj_eq THEN' rtac (worel RS @{thm wo_rel.adm_wo_def}) THEN'
     REPEAT_DETERM_N 3 o rtac allI THEN' rtac impI THEN'
     CONJ_WRAP_GEN' (EVERY' [rtac Pair_eqI, rtac conjI]) minH_tac in_congs) 1
   end;
 
-fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [stac @{thm relChain_def}, rtac allI, rtac allI,
-  rtac impI, rtac @{thm case_split}, rtac @{thm xt1(3)}, rtac min_algs, etac @{thm FieldI2},
-  rtac subsetI, rtac UnI1, rtac @{thm UN_I}, etac @{thm underS_I}, atac, atac,
-  rtac equalityD1, dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1;
+fun mk_min_algs_mono_tac ctxt min_algs = EVERY' [rtac relChainD, rtac allI, rtac allI, rtac impI,
+  rtac @{thm case_split}, rtac @{thm xt1(3)}, rtac min_algs, etac @{thm FieldI2}, rtac subsetI,
+  rtac UnI1, rtac @{thm UN_I}, etac @{thm underS_I}, atac, atac, rtac equalityD1,
+  dtac @{thm notnotD}, hyp_subst_tac ctxt, rtac refl] 1;
 
 fun mk_min_algs_card_of_tac cT ct m worel min_algs in_bds bd_Card_order bd_Cnotzero
   suc_Card_order suc_Cinfinite suc_Cnotzero suc_Asuc Asuc_Cinfinite =
@@ -370,13 +373,14 @@
   end;
 
 fun mk_card_of_min_alg_tac min_alg_def card_of suc_Card_order suc_Asuc Asuc_Cinfinite =
-  EVERY' [stac min_alg_def, rtac @{thm UNION_Cinfinite_bound},
-    rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_Field_ordIso}, rtac suc_Card_order,
-    rtac @{thm ordLess_imp_ordLeq}, rtac suc_Asuc, rtac ballI, dtac rev_mp, rtac card_of,
-    REPEAT_DETERM o etac conjE, atac, rtac Asuc_Cinfinite] 1;
+  EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac (min_alg_def RS @{thm card_of_ordIso_subst}),
+    rtac @{thm UNION_Cinfinite_bound}, rtac @{thm ordIso_ordLeq_trans},
+    rtac @{thm card_of_Field_ordIso}, rtac suc_Card_order, rtac @{thm ordLess_imp_ordLeq},
+    rtac suc_Asuc, rtac ballI, dtac rev_mp, rtac card_of,  REPEAT_DETERM o etac conjE, atac,
+    rtac Asuc_Cinfinite] 1;
 
 fun mk_least_min_alg_tac min_alg_def least =
-  EVERY' [stac min_alg_def, rtac @{thm UN_least}, dtac least, dtac mp, atac,
+  EVERY' [rtac (min_alg_def RS ord_eq_le_trans), rtac @{thm UN_least}, dtac least, dtac mp, atac,
     REPEAT_DETERM o etac conjE, atac] 1;
 
 fun mk_alg_select_tac ctxt Abs_inverse =
@@ -393,24 +397,25 @@
       CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs;
     fun alg_epi_tac ((alg_set, str_init_def), set_map) =
       EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
-        rtac ballI, ftac (alg_select RS bspec), stac str_init_def, etac alg_set,
-        REPEAT_DETERM o EVERY' [rtac ord_eq_le_trans, resolve_tac set_map, rtac subset_trans,
-            etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec, atac]];
+        rtac ballI, ftac (alg_select RS bspec), rtac (str_init_def RS @{thm ssubst_mem}),
+        etac alg_set, REPEAT_DETERM o EVERY' [rtac ord_eq_le_trans, resolve_tac set_map,
+          rtac subset_trans, etac @{thm image_mono}, rtac @{thm image_Collect_subsetI}, etac bspec,
+          atac]];
   in
-    (rtac mor_cong THEN' REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm comp_id}) THEN'
-    rtac (Thm.permute_prems 0 1 mor_comp) THEN' etac (Thm.permute_prems 0 1 mor_comp) THEN'
-    stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' rtac mor_incl_min_alg THEN'
-    stac alg_def THEN' CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)) 1
+    EVERY' [rtac mor_cong, REPEAT_DETERM_N n o (rtac sym THEN' rtac @{thm comp_id}),
+      rtac (Thm.permute_prems 0 1 mor_comp), etac (Thm.permute_prems 0 1 mor_comp),
+      rtac (mor_def RS iffD2), rtac conjI, fbetw_tac, mor_tac, rtac mor_incl_min_alg,
+      rtac (alg_def RS iffD2), CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)] 1
   end;
 
 fun mk_init_ex_mor_tac ctxt Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
     mor_comp mor_select mor_incl_min_alg =
   let
     val n = length card_of_min_algs;
-    val card_of_ordIso_tac = EVERY' [rtac ssubst, rtac @{thm card_of_ordIso},
+    val card_of_ordIso_tac = EVERY' [rtac iffD2, rtac @{thm card_of_ordIso},
       rtac @{thm ordIso_symmetric}, rtac conjunct1, rtac conjunct2, atac];
-    fun internalize_tac card_of = EVERY' [rtac subst, rtac @{thm internalize_card_of_ordLeq2},
-      rtac @{thm ordLeq_ordIso_trans}, rtac card_of, rtac subst,
+    fun internalize_tac card_of = EVERY' [rtac iffD1, rtac @{thm internalize_card_of_ordLeq2},
+      rtac @{thm ordLeq_ordIso_trans}, rtac card_of, rtac iffD1,
       rtac @{thm Card_order_iff_ordIso_card_of}, rtac @{thm Card_order_cexp}];
   in
     (rtac rev_mp THEN'
@@ -451,7 +456,7 @@
 
     fun mk_unique_tac (k, least_min_alg) =
       select_prem_tac n (etac @{thm prop_restrict}) k THEN' rtac least_min_alg THEN'
-      stac alg_def THEN'
+      rtac (alg_def RS iffD2) THEN'
       CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s)));
   in
     CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1
@@ -471,7 +476,7 @@
 
     fun mk_induct_tac least_min_alg =
       rtac ballI THEN' etac @{thm prop_restrict} THEN' rtac least_min_alg THEN'
-      stac alg_def THEN'
+      rtac (alg_def RS iffD2) THEN'
       CONJ_WRAP' mk_alg_tac alg_sets;
   in
     CONJ_WRAP' mk_induct_tac least_min_algs 1
@@ -507,8 +512,8 @@
   end;
 
 fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
-  EVERY' [stac dtor_def, rtac @{thm ext}, rtac trans, rtac o_apply, rtac trans, rtac foldx,
-    rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
+  EVERY' [rtac @{thm ext}, rtac trans, rtac o_apply, rtac (dtor_def RS fun_cong RS trans),
+    rtac trans, rtac foldx, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
     EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
       ctor_o_folds),
     rtac sym, rtac id_apply] 1;
@@ -530,18 +535,18 @@
     val ks = 1 upto n;
 
     fun mk_IH_tac Rep_inv Abs_inv set_map =
-      DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS subst), etac bspec,
+      DETERM o EVERY' [dtac meta_mp, rtac (Rep_inv RS arg_cong RS iffD1), etac bspec,
         dtac set_rev_mp, rtac equalityD1, rtac set_map, etac imageE,
-        hyp_subst_tac ctxt, rtac (Abs_inv RS ssubst), etac set_mp, atac, atac];
+        hyp_subst_tac ctxt, rtac (Abs_inv RS @{thm ssubst_mem}), etac set_mp, atac, atac];
 
     fun mk_closed_tac (k, (morE, set_maps)) =
       EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
-        rtac (mor_Abs RS morE RS arg_cong RS ssubst), atac,
+        rtac (mor_Abs RS morE RS arg_cong RS iffD2), atac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec},
         EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac];
 
     fun mk_induct_tac (Rep, Rep_inv) =
-      EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RSN (2, bspec))];
+      EVERY' [rtac (Rep_inv RS arg_cong RS iffD1), etac (Rep RSN (2, bspec))];
   in
     (rtac mp THEN' rtac impI THEN'
     DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'