--- 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)"