# HG changeset patch
# User wenzelm
# Date 1703354915 -3600
# Node ID 3ef7606a0d11a99280e59c8d60b1c75e00723692
# Parent  8eb7e325f40dbfe1a2acf3fdf66a7c5143cdc69f
eliminate duplicate (see also 6cbcfac5b72e and af7b79271364);

diff -r 8eb7e325f40d -r 3ef7606a0d11 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Sat Dec 23 16:12:53 2023 +0100
+++ b/src/ZF/upair.thy	Sat Dec 23 19:08:35 2023 +0100
@@ -18,10 +18,6 @@
 
 ML_file \<open>Tools/typechk.ML\<close>
 
-lemma atomize_ball [symmetric, rulify]:
-     "(\<And>x. x \<in> A \<Longrightarrow> P(x)) \<equiv> Trueprop (\<forall>x\<in>A. P(x))"
-by (simp add: Ball_def atomize_all atomize_imp)
-
 
 subsection\<open>Unordered Pairs: constant \<^term>\<open>Upair\<close>\<close>