src/ZF/ZF.thy

--- a/src/ZF/ZF.thy	Fri Jun 11 16:52:17 2010 +0200
+++ b/src/ZF/ZF.thy	Fri Jun 11 17:14:01 2010 +0200
@@ -199,10 +199,7 @@
 finalconsts
   0 Pow Inf Union PrimReplace mem
 
-defs 
-(*don't try to use constdefs: the declaration order is tightly constrained*)
-
-  (* Bounded Quantifiers *)
+defs  (* Bounded Quantifiers *)
   Ball_def:      "Ball(A, P) == \<forall>x. x\<in>A --> P(x)"
   Bex_def:       "Bex(A, P) == \<exists>x. x\<in>A & P(x)"