Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
changeset 61424 c3658c18b7bc
parent 61334 8d40ddaa427f
child 61841 4d3527b94f2a 
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -698,7 +698,7 @@
     1.4                (fn (active_set_map0, in_Irel) => EVERY' [rtac ctxt ord_eq_le_trans,
     1.5                  rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt active_set_map0, rtac ctxt @{thm UN_least},
     1.6                  dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
     1.7 -                dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
     1.8 +                dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
     1.9                  REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
    1.10                    @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
    1.11                  hyp_subst_tac ctxt,
    1.12 @@ -712,7 +712,7 @@
    1.13            REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
    1.14            EVERY' (map (fn in_Irel => EVERY' [rtac ctxt trans, rtac ctxt o_apply,
    1.15              dtac ctxt set_rev_mp, assume_tac ctxt,
    1.16 -            dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
    1.17 +            dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
    1.18              REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
    1.19                @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
    1.20              hyp_subst_tac ctxt,
isabelle