src/CCL/Set.thy

--- a/src/CCL/Set.thy	Mon Oct 20 10:39:26 1997 +0200
+++ b/src/CCL/Set.thy	Mon Oct 20 10:48:22 1997 +0200
@@ -7,6 +7,8 @@
 
 Set = FOL +
 
+global
+
 types
   'a set
 
@@ -28,6 +30,7 @@
   empty         :: "'a set"                             ("{}")
   "oo"          :: "['b => 'c, 'a => 'b, 'a] => 'c"     (infixr 50) (*composition*)
 
+syntax
   "@Coll"       :: "[idt, o] => 'a set"                 ("(1{_./ _})") (*collection*)
 
   (* Big Intersection / Union *)
@@ -48,6 +51,7 @@
   "ALL x:A. P"  == "Ball(A, %x. P)"
   "EX x:A. P"   == "Bex(A, %x. P)"
 
+local
 
 rules
   mem_Collect_iff       "(a : {x. P(x)}) <-> P(a)"