# HG changeset patch
# User lcp
# Date 799319861 -7200
# Node ID 2f9f2ea26f8fa48c53737bc843a65addefd045f5
# Parent  e57beb974dd77d7a384aedfdb51c8ec98447876b
Simplified proof of Hausdorff_next_exists.

diff -r e57beb974dd7 -r 2f9f2ea26f8f src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Fri Apr 28 15:38:15 1995 +0200
+++ b/src/ZF/Zorn.ML	Mon May 01 11:17:41 1995 +0200
@@ -204,8 +204,6 @@
 			    chain_subset_Pow RS subsetD,
 			    choice_super]) 1);
 (*Now, verify that it increases*)
-by (rtac allI 1);
-by (rtac impI 1);
 by (asm_simp_tac (ZF_ss addsimps [Pow_iff, subset_refl]
                         setloop split_tac [expand_if]) 1);
 by (safe_tac ZF_cs);