strengthened tactic
authorblanchet
Mon Nov 04 11:59:08 2013 +0100 (2013-11-04)
changeset 54241357988ad95ec
parent 54240 756ff45e08ba
child 54242 99ef8036fb3d
strengthened tactic
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Nov 04 11:03:13 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Nov 04 11:59:08 2013 +0100
     1.3 @@ -151,8 +151,8 @@
     1.4    (atac ORELSE' REPEAT o etac conjE THEN'
     1.5       full_simp_tac
     1.6         (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
     1.7 -     REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN' REPEAT o rtac conjI THEN'
     1.8 -     REPEAT o (rtac refl ORELSE' atac));
     1.9 +     REPEAT o etac conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN'
    1.10 +     REPEAT o (resolve_tac [refl, conjI] ORELSE' atac));
    1.11  
    1.12  fun mk_coinduct_distinct_ctrs_tac ctxt discs discs' =
    1.13    let
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Nov 04 11:03:13 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Nov 04 11:59:08 2013 +0100
     2.3 @@ -715,8 +715,8 @@
     2.4           sel_corecs = sel_corecs}
     2.5        end;
     2.6  
     2.7 -    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss
     2.8 -        coiter_thmsss disc_coitersss sel_coiterssss =
     2.9 +    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss coiter_thmsss
    2.10 +        disc_coitersss sel_coiterssss =
    2.11        let
    2.12          val ctrs = #ctrs (nth ctr_sugars index);
    2.13          val discs = #discs (nth ctr_sugars index);