src/HOL/Lambda/Eta.thy
changeset 11183 0476c6e07bca
parent 9941 fe05af7ec816
child 11638 2c3dee321b4b
     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