src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 50058 bb1fadeba35e
parent 49684 1cf810b8f600
child 51070 6ca703425c01
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Nov 13 09:08:32 2012 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Nov 13 12:06:43 2012 +0100
     1.3 @@ -658,7 +658,7 @@
     1.4        REPEAT_DETERM o rtac allI,
     1.5        CONJ_WRAP' (fn Lev_0 =>
     1.6          EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
     1.7 -          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefix_Nil[THEN subst, of "%x. x"]},
     1.8 +          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
     1.9            hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
    1.10            rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
    1.11        REPEAT_DETERM o rtac allI,
    1.12 @@ -666,7 +666,7 @@
    1.13          EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
    1.14            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
    1.15              (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
    1.16 -              dtac @{thm prefix_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
    1.17 +              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
    1.18                rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
    1.19                rtac Lev_0, rtac @{thm singletonI},
    1.20                REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
    1.21 @@ -857,7 +857,7 @@
    1.22          rtac conjI,
    1.23            rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,
    1.24            rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},
    1.25 -          etac @{thm prefix_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
    1.26 +          etac @{thm prefixeq_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
    1.27          rtac conjI,
    1.28            rtac ballI, etac @{thm UN_E}, rtac conjI,
    1.29            if n = 1 then K all_tac else rtac (mk_sumEN n),