1.1 --- a/src/HOL/Lambda/Eta.thy	Mon Feb 26 10:41:24 2001 +0100
     1.2 +++ b/src/HOL/Lambda/Eta.thy	Mon Feb 26 16:36:53 2001 +0100
     1.3 @@ -163,7 +163,7 @@
     1.4      "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
     1.5    apply (induct_tac u)
     1.6      apply (simp_all add: subst_Var)
     1.7 -    apply (blast intro: r_into_rtrancl)
     1.8 +    apply (blast)
     1.9     apply (blast intro: rtrancl_eta_App)
    1.10    apply (blast intro!: rtrancl_eta_Abs eta_lift)
    1.11    done
    1.12 @@ -172,10 +172,11 @@
    1.13    apply (unfold square_def)
    1.14    apply (rule impI [THEN allI [THEN allI]])
    1.15    apply (erule beta.induct)
    1.16 -     apply (slowsimp intro: r_into_rtrancl rtrancl_eta_subst eta_subst)
    1.17 -    apply (blast intro: r_into_rtrancl rtrancl_eta_AppL)
    1.18 -   apply (blast intro: r_into_rtrancl rtrancl_eta_AppR)
    1.19 -  apply (slowsimp intro: r_into_rtrancl rtrancl_eta_Abs free_beta
    1.20 +     apply (slowsimp intro: rtrancl_eta_subst eta_subst)
    1.21 +    apply (blast intro: rtrancl_eta_AppL)
    1.22 +   apply (blast intro: rtrancl_eta_AppR)
    1.23 +  apply simp;
    1.24 +  apply (slowsimp intro: rtrancl_eta_Abs free_beta
    1.25      iff del: dB.distinct simp: dB.distinct)    (*23 seconds?*)
    1.26    done
    1.27  

     2.1 --- a/src/HOL/Lambda/ListBeta.thy	Mon Feb 26 10:41:24 2001 +0100
     2.2 +++ b/src/HOL/Lambda/ListBeta.thy	Mon Feb 26 16:36:53 2001 +0100
     2.3 @@ -60,13 +60,13 @@
     2.4      apply (split split_if_asm)
     2.5       apply simp
     2.6       apply blast
     2.7 -    apply (force intro: disjI1 [THEN append_step1I])
     2.8 +    apply (force intro!: disjI1 [THEN append_step1I])
     2.9     apply (clarify del: disjCI)
    2.10     apply (drule App_eq_foldl_conv [THEN iffD1])
    2.11     apply (split split_if_asm)
    2.12      apply simp
    2.13      apply blast
    2.14 -   apply (auto 0 3 intro: disjI2 [THEN append_step1I])
    2.15 +   apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
    2.16    done
    2.17  
    2.18  lemma apps_betasE [elim!]: