--- 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;