--- a/src/HOL/Set.thy Thu Sep 29 00:58:54 2005 +0200
+++ b/src/HOL/Set.thy Thu Sep 29 00:58:55 2005 +0200
@@ -305,6 +305,9 @@
axioms
mem_Collect_eq: "(a : {x. P(x)}) = P(a)"
Collect_mem_eq: "{x. x:A} = A"
+finalconsts
+ Collect
+ "op :"
defs
Ball_def: "Ball A P == ALL x. x:A --> P(x)"