src/HOL/Set.thy
changeset 17702 ea88ddeafabe
parent 17589 58eeffd73be1
child 17715 68583762ebdb
--- 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)"