# HG changeset patch
# User lcp
# Date 779103640 -7200
# Node ID d4c6e2bdde59a7fbd9dc7a8cf84ae780a1076e44
# Parent  9154d8410514822f27745f8ed4a05b913f59f671
ZF/Zorn/next_bounded: deleted this proof, which was already in comments

diff -r 9154d8410514 -r d4c6e2bdde59 src/ZF/Zorn.ML
--- a/src/ZF/Zorn.ML	Thu Sep 08 13:17:57 1994 +0200
+++ b/src/ZF/Zorn.ML	Fri Sep 09 11:40:40 1994 +0200
@@ -36,14 +36,6 @@
 by (assume_tac 1);
 val increasingD2 = result();
 
-(*????????????????????????????????????????????????????????????????
-goal Zorn.thy
-    "!!next S. [| X : Pow(S);  next: increasing(S) |] ==> next`X : Pow(S)";
-by (eresolve_tac [increasingD1 RS apply_type] 1);
-by (assume_tac 1);
-val next_bounded = result();
-*)
-
 (*Introduction rules*)
 val [TFin_nextI, Pow_TFin_UnionI] = TFin.intrs;
 val TFin_UnionI = PowI RS Pow_TFin_UnionI;