1.1 --- a/src/CCL/Set.thy	Thu Jul 23 21:59:56 2009 +0200
     1.2 +++ b/src/CCL/Set.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -40,11 +40,11 @@
     1.4    "@Bex"        :: "[idt, 'a set, o] => o"              ("(EX _:_./ _)" [0, 0, 0] 10)
     1.5  
     1.6  translations
     1.7 -  "{x. P}"      == "Collect(%x. P)"
     1.8 -  "INT x:A. B"  == "INTER(A, %x. B)"
     1.9 -  "UN x:A. B"   == "UNION(A, %x. B)"
    1.10 -  "ALL x:A. P"  == "Ball(A, %x. P)"
    1.11 -  "EX x:A. P"   == "Bex(A, %x. P)"
    1.12 +  "{x. P}"      == "CONST Collect(%x. P)"
    1.13 +  "INT x:A. B"  == "CONST INTER(A, %x. B)"
    1.14 +  "UN x:A. B"   == "CONST UNION(A, %x. B)"
    1.15 +  "ALL x:A. P"  == "CONST Ball(A, %x. P)"
    1.16 +  "EX x:A. P"   == "CONST Bex(A, %x. P)"
    1.17  
    1.18  local
    1.19