--- a/src/CCL/Set.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/CCL/Set.thy Mon Feb 08 21:28:27 2010 +0100
@@ -40,11 +40,11 @@
"@Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10)
translations
- "{x. P}" == "Collect(%x. P)"
- "INT x:A. B" == "INTER(A, %x. B)"
- "UN x:A. B" == "UNION(A, %x. B)"
- "ALL x:A. P" == "Ball(A, %x. P)"
- "EX x:A. P" == "Bex(A, %x. P)"
+ "{x. P}" == "CONST Collect(%x. P)"
+ "INT x:A. B" == "CONST INTER(A, %x. B)"
+ "UN x:A. B" == "CONST UNION(A, %x. B)"
+ "ALL x:A. P" == "CONST Ball(A, %x. P)"
+ "EX x:A. P" == "CONST Bex(A, %x. P)"
local