eliminated alias;
authorwenzelm
Fri Jul 24 22:29:06 2015 +0200 (2015-07-24)
changeset 60777ee811a49c8f6
parent 60776 2164e7b47454
child 60778 682c0dd89b26
eliminated alias;
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Jul 24 22:20:22 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Jul 24 22:29:06 2015 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4                EVERY' [rtac ctxt sym, rtac ctxt trans, rtac ctxt (refl RSN (2, @{thm SUP_cong})),
     1.5                  etac ctxt (morE RS sym RS arg_cong RS trans), assume_tac ctxt, rtac ctxt set_map0,
     1.6                  rtac ctxt (@{thm UN_simps(10)} RS trans), rtac ctxt (refl RS @{thm SUP_cong}),
     1.7 -                ftac ctxt coalg_set, assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt,
     1.8 +                forward_tac ctxt [coalg_set], assume_tac ctxt, dtac ctxt set_mp, assume_tac ctxt,
     1.9                  rtac ctxt mp, rtac ctxt (mk_conjunctN n i),
    1.10                  REPEAT_DETERM o etac ctxt allE, assume_tac ctxt, assume_tac ctxt])
    1.11              (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
    1.12 @@ -418,7 +418,7 @@
    1.13    end;
    1.14  
    1.15  fun mk_length_Lev'_tac ctxt length_Lev =
    1.16 -  EVERY' [ftac ctxt length_Lev, etac ctxt ssubst, assume_tac ctxt] 1;
    1.17 +  EVERY' [forward_tac ctxt [length_Lev], etac ctxt ssubst, assume_tac ctxt] 1;
    1.18  
    1.19  fun mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss =
    1.20    let
    1.21 @@ -720,7 +720,7 @@
    1.22    let
    1.23      val n = length Rep_injects;
    1.24    in
    1.25 -    EVERY' [rtac ctxt rev_mp, ftac ctxt (bis_def RS iffD1),
    1.26 +    EVERY' [rtac ctxt rev_mp, forward_tac ctxt [bis_def RS iffD1],
    1.27        REPEAT_DETERM o etac ctxt conjE, rtac ctxt bis_cong, rtac ctxt bis_O, rtac ctxt bis_converse,
    1.28        rtac ctxt bis_Gr, rtac ctxt tcoalg, rtac ctxt mor_Rep, rtac ctxt bis_O, assume_tac ctxt,
    1.29        rtac ctxt bis_Gr, rtac ctxt tcoalg,
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Jul 24 22:20:22 2015 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Jul 24 22:29:06 2015 +0200
     2.3 @@ -340,7 +340,8 @@
     2.4        CONJ_WRAP' (fn thm => EVERY' [rtac ctxt ballI, rtac ctxt thm]) str_init_defs;
     2.5      fun alg_epi_tac ((alg_set, str_init_def), set_map) =
     2.6        EVERY' [rtac ctxt ballI, REPEAT_DETERM o eresolve_tac ctxt [CollectE, conjE], rtac ctxt CollectI,
     2.7 -        rtac ctxt ballI, ftac ctxt (alg_select RS bspec), rtac ctxt (str_init_def RS @{thm ssubst_mem}),
     2.8 +        rtac ctxt ballI, forward_tac ctxt [alg_select RS bspec],
     2.9 +        rtac ctxt (str_init_def RS @{thm ssubst_mem}),
    2.10          etac ctxt alg_set, REPEAT_DETERM o EVERY' [rtac ctxt ord_eq_le_trans, resolve_tac ctxt set_map,
    2.11            rtac ctxt subset_trans, etac ctxt @{thm image_mono}, rtac ctxt @{thm image_Collect_subsetI}, etac ctxt bspec,
    2.12            assume_tac ctxt]];
     3.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Jul 24 22:20:22 2015 +0200
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Fri Jul 24 22:29:06 2015 +0200
     3.3 @@ -57,7 +57,6 @@
     3.4    val rtac: Proof.context -> thm -> int -> tactic
     3.5    val etac: Proof.context -> thm -> int -> tactic
     3.6    val dtac: Proof.context -> thm -> int -> tactic
     3.7 -  val ftac: Proof.context -> thm -> int -> tactic
     3.8  
     3.9    val list_all_free: term list -> term -> term
    3.10    val list_exists_free: term list -> term -> term
    3.11 @@ -281,6 +280,5 @@
    3.12  fun rtac ctxt thm = resolve_tac ctxt [thm];
    3.13  fun etac ctxt thm = eresolve_tac ctxt [thm];
    3.14  fun dtac ctxt thm = dresolve_tac ctxt [thm];
    3.15 -fun ftac ctxt thm = forward_tac ctxt [thm];
    3.16  
    3.17  end;