# HG changeset patch
# User paulson
# Date 983201813 -3600
# Node ID 0476c6e07bca395f43caa9e88797649957f87123
# Parent  e123a50aa949022fcbacf9c80dd57fa7e7a5b576
minor tweaks to speed the proofs

diff -r e123a50aa949 -r 0476c6e07bca src/HOL/Lambda/Eta.thy
--- 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
 
diff -r e123a50aa949 -r 0476c6e07bca src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Mon Feb 26 10:41:24 2001 +0100
+++ b/src/HOL/Lambda/ListBeta.thy	Mon Feb 26 16:36:53 2001 +0100
@@ -60,13 +60,13 @@
     apply (split split_if_asm)
      apply simp
      apply blast
-    apply (force intro: disjI1 [THEN append_step1I])
+    apply (force intro!: disjI1 [THEN append_step1I])
    apply (clarify del: disjCI)
    apply (drule App_eq_foldl_conv [THEN iffD1])
    apply (split split_if_asm)
     apply simp
     apply blast
-   apply (auto 0 3 intro: disjI2 [THEN append_step1I])
+   apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
   done
 
 lemma apps_betasE [elim!]: