# HG changeset patch
# User wenzelm
# Date 1138559032 -3600
# Node ID 6cbcfac5b72e1c32bdeb9d69a815db9faea1587e
# Parent  9dd7898410184fab8894b6fd22c5b216db6faa4b
declare atomize/defn for Ball;

diff -r 9dd789841018 -r 6cbcfac5b72e src/ZF/ZF.thy
--- 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*}