# HG changeset patch
# User paulson
# Date 962181734 -7200
# Node ID 647d554a65ae0656a4db8bc904740aedfb115cb1
# Parent  cee6d5aee7c8b462e1aa636c6117c2b62fc94727
tidied a monstrous proof

diff -r cee6d5aee7c8 -r 647d554a65ae src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Wed Jun 28 10:41:16 2000 +0200
+++ b/src/HOL/Univ.ML	Wed Jun 28 10:42:14 2000 +0200
@@ -380,23 +380,7 @@
 
 Goalw [Lim_def] "Lim f = Lim g ==> f = g";
 by (rtac ext 1);
-by (rtac ccontr 1);
-by (etac equalityE 1);
-by (subgoal_tac "? y. y : f x & y ~: g x | y ~: f x & y : g x" 1);
-by (Blast_tac 2);
-by (etac exE 1);
-by (etac disjE 1);
-by (REPEAT (EVERY [
-  dtac subsetD 1,
-  Fast_tac 1,
-  etac UnionE 1,
-  dtac CollectD 1,
-  etac exE 1,
-  hyp_subst_tac 1,
-  etac imageE 1,
-  etac Push_Node_inject 1,
-  Asm_full_simp_tac 1,
-  TRY (thin_tac "?S <= ?T" 1)]));
+by (blast_tac (claset() addSEs [Push_Node_inject]) 1);
 qed "Lim_inject";
 
 Goalw [Funs_def] "S <= T ==> Funs S <= Funs T";