declare atomize/defn for Ball;

--- a/src/ZF/ZF.thy	Sun Jan 29 19:23:51 2006 +0100
+++ b/src/ZF/ZF.thy	Sun Jan 29 19:23:52 2006 +0100
@@ -336,6 +336,13 @@
     "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))"
 by (simp add: Ball_def)
 
+lemma atomize_ball:
+    "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"
+  by (simp only: Ball_def atomize_all atomize_imp)
+
+lemmas [symmetric, rulify] = atomize_ball
+  and [symmetric, defn] = atomize_ball
+
 
 subsection{*Bounded existential quantifier*}