src/CCL/Set.thy

--- a/src/CCL/Set.thy	Tue Aug 17 17:57:19 2010 +0100
+++ b/src/CCL/Set.thy	Tue Aug 17 19:36:38 2010 +0200
@@ -4,8 +4,6 @@
 imports FOL
 begin
 
-global
-
 typedecl 'a set
 arities set :: ("term") "term"
 
@@ -46,8 +44,6 @@
   "ALL x:A. P"  == "CONST Ball(A, %x. P)"
   "EX x:A. P"   == "CONST Bex(A, %x. P)"
 
-local
-
 axioms
   mem_Collect_iff:       "(a : {x. P(x)}) <-> P(a)"
   set_extension:         "A=B <-> (ALL x. x:A <-> x:B)"