src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 49684 1cf810b8f600
parent 49585 5c4a12550491
child 50058 bb1fadeba35e
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Oct 02 01:00:18 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Oct 02 09:20:28 2012 +0200
     1.3 @@ -288,12 +288,12 @@
     1.4          REPEAT_DETERM o etac conjE,
     1.5          hyp_subst_tac,
     1.6          REPEAT_DETERM o eresolve_tac [CollectE, conjE],
     1.7 -        rtac bexI, rtac conjI, rtac trans, rtac map_comp,
     1.8 -        REPEAT_DETERM_N m o stac @{thm id_o},
     1.9 -        REPEAT_DETERM_N n o stac @{thm o_id},
    1.10 -        etac sym, rtac trans, rtac map_comp,
    1.11 -        REPEAT_DETERM_N m o stac @{thm id_o},
    1.12 -        REPEAT_DETERM_N n o stac @{thm o_id},
    1.13 +        rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
    1.14 +        REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
    1.15 +        REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
    1.16 +        etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
    1.17 +        REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
    1.18 +        REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
    1.19          rtac trans, rtac map_cong,
    1.20          REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac],
    1.21          REPEAT_DETERM_N n o rtac refl,