eliminate duplicate (see also 6cbcfac5b72e and af7b79271364);
authorwenzelm
Sat, 23 Dec 2023 19:08:35 +0100
changeset 79340 3ef7606a0d11
parent 79339 8eb7e325f40d
child 79341 e8d7b7d5390d
eliminate duplicate (see also 6cbcfac5b72e and af7b79271364);
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>