# HG changeset patch
# User paulson
# Date 905441213 -7200
# Node ID 6712d95c811342380b4c775d61ef2983be44b419
# Parent  a0b16470c502f5c4393fdeea9f34b2fedc7c71a9
tidied, eliminating hard proof

diff -r a0b16470c502 -r 6712d95c8113 src/HOL/Lambda/ListBeta.ML
--- a/src/HOL/Lambda/ListBeta.ML	Thu Sep 10 17:26:16 1998 +0200
+++ b/src/HOL/Lambda/ListBeta.ML	Thu Sep 10 17:26:53 1998 +0200
@@ -56,18 +56,15 @@
 by (Asm_full_simp_tac 1);
 val lemma = result();
 
-Goal "[| r$$rs -> s; \
-\        !r'. r -> r' --> s = r'$$rs --> R; \
-\        !rs'. rs => rs' --> s = r$$rs' --> R; \
-\        !t u us. r = Abs t --> rs = u#us --> s = t[u/0]$$us --> R \
-\     |] ==> R";
-by (dtac lemma 1);
-by (blast_tac HOL_cs 1);
-val lemma = result();
-bind_thm("apps_betasE",
-          impI RSN (4,impI RSN (4,impI RSN (4,allI RSN (4,allI RSN (4,allI RSN (4,
-          impI RSN (3,impI RSN (3,allI RSN (3,
-          impI RSN (2,impI RSN (2,allI RSN (2,lemma)))))))))))));
+val major::prems =
+Goal "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;   \
+\        !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;              \
+\        !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]   \
+\     ==> R";
+by (cut_facts_tac [major RS lemma RS spec RS spec] 1);
+by (REPEAT_FIRST (ares_tac [refl] ORELSE'
+		  eresolve_tac (prems @ [exE, conjE, impE, disjE])));
+qed "apps_betasE";
 AddSEs [apps_betasE];
 
 Goal "r -> s ==> r$$ss -> s$$ss";