--- a/src/HOL/Lambda/Eta.thy Mon Feb 26 10:41:24 2001 +0100
+++ b/src/HOL/Lambda/Eta.thy Mon Feb 26 16:36:53 2001 +0100
@@ -163,7 +163,7 @@
"\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
apply (induct_tac u)
apply (simp_all add: subst_Var)
- apply (blast intro: r_into_rtrancl)
+ apply (blast)
apply (blast intro: rtrancl_eta_App)
apply (blast intro!: rtrancl_eta_Abs eta_lift)
done
@@ -172,10 +172,11 @@
apply (unfold square_def)
apply (rule impI [THEN allI [THEN allI]])
apply (erule beta.induct)
- apply (slowsimp intro: r_into_rtrancl rtrancl_eta_subst eta_subst)
- apply (blast intro: r_into_rtrancl rtrancl_eta_AppL)
- apply (blast intro: r_into_rtrancl rtrancl_eta_AppR)
- apply (slowsimp intro: r_into_rtrancl rtrancl_eta_Abs free_beta
+ apply (slowsimp intro: rtrancl_eta_subst eta_subst)
+ apply (blast intro: rtrancl_eta_AppL)
+ apply (blast intro: rtrancl_eta_AppR)
+ apply simp;
+ apply (slowsimp intro: rtrancl_eta_Abs free_beta
iff del: dB.distinct simp: dB.distinct) (*23 seconds?*)
done