src/CCL/Set.thy

--- a/src/CCL/Set.thy	Tue Mar 29 23:15:25 2011 +0200
+++ b/src/CCL/Set.thy	Tue Mar 29 23:27:38 2011 +0200
@@ -46,9 +46,9 @@
   "ALL x:A. P"  == "CONST Ball(A, %x. P)"
   "EX x:A. P"   == "CONST Bex(A, %x. P)"
 
-axioms
-  mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
-  set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"
+axiomatization where
+  mem_Collect_iff: "(a : {x. P(x)}) <-> P(a)" and
+  set_extension: "A = B <-> (ALL x. x:A <-> x:B)"
 
 defs
   Ball_def:      "Ball(A, P)  == ALL x. x:A --> P(x)"