--- a/src/HOL/Set.thy Tue Aug 16 15:36:28 2005 +0200
+++ b/src/HOL/Set.thy Tue Aug 16 18:53:11 2005 +0200
@@ -303,8 +303,8 @@
text {* Isomorphisms between predicates and sets. *}
axioms
- mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)"
- Collect_mem_eq [simp]: "{x. x:A} = A"
+ mem_Collect_eq: "(a : {x. P(x)}) = P(a)"
+ Collect_mem_eq: "{x. x:A} = A"
defs
Ball_def: "Ball A P == ALL x. x:A --> P(x)"
@@ -334,6 +334,8 @@
subsubsection {* Relating predicates and sets *}
+declare mem_Collect_eq [iff] Collect_mem_eq [simp]
+
lemma CollectI: "P(a) ==> a : {x. P(x)}"
by simp