# HG changeset patch
# User paulson
# Date 962273803 -7200
# Node ID 379b0c3f7c852d1c534456adbbcaf355702ee616
# Parent  68ecc04785f130ecedf0d2438eabcf5a83efea33
tidied

diff -r 68ecc04785f1 -r 379b0c3f7c85 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Thu Jun 29 12:15:08 2000 +0200
+++ b/src/HOL/Induct/Mutil.ML	Thu Jun 29 12:16:43 2000 +0200
@@ -92,7 +92,7 @@
 (*this lemma tells us that both "inserts" are non-trivial*)
 by (subgoal_tac "ALL p C. C Int a = {p} --> p ~: t" 1);
 by (Asm_simp_tac 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
+by (Blast_tac 1);
 qed "tiling_domino_0_1";
 
 (*Final argument is surprisingly complex*)
diff -r 68ecc04785f1 -r 379b0c3f7c85 src/HOL/Real/Hyperreal/Zorn.ML
--- a/src/HOL/Real/Hyperreal/Zorn.ML	Thu Jun 29 12:15:08 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML	Thu Jun 29 12:16:43 2000 +0200
@@ -237,11 +237,7 @@
 by (subgoal_tac "({u} Un c): super S c" 1);
 by (Asm_full_simp_tac 1);
 by (rewrite_tac [super_def,psubset_def]);
-by Safe_tac;
-by (fast_tac (claset() addEs [chain_extend]) 1);
-by (subgoal_tac "u ~: c" 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
-by (blast_tac (claset() addDs [chain_Union_upper]) 1);
+by (blast_tac (claset() addIs [chain_extend] addDs [chain_Union_upper]) 1);
 qed "maxchain_Zorn";
 
 Goal "ALL c: chain S. Union(c): S ==> \
@@ -270,12 +266,7 @@
 by (forw_inst_tac [("z","x")]  chain_extend 1);
 by (assume_tac 1 THEN Blast_tac 1);
 by (rewrite_tac [maxchain_def,super_def,psubset_def]);
-by (Step_tac 1);
-by (eres_inst_tac [("c","{x} Un c")] equalityCE 1);
-by (Step_tac 1);
-by (subgoal_tac "x ~: c" 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
-by (Blast_tac 1);
+by (blast_tac (claset() addSEs [equalityCE]) 1);
 qed "Zorn_Lemma2";
 
 (** misc. lemmas **)