--- a/src/HOL/Analysis/Metric_Arith.thy Sun Oct 27 12:09:07 2019 -0400
+++ b/src/HOL/Analysis/Metric_Arith.thy Sun Oct 27 12:13:04 2019 -0400
@@ -67,6 +67,9 @@
lemmas nnf_simps = nnf_thms linorder_not_less linorder_not_le
declare nnf_simps[metric_nnf]
+lemma ball_insert: "(\<forall>x\<in>insert a B. P x) = (P a \<and> (\<forall>x\<in>B. P x))"
+ by blast
+
lemma Sup_insert_insert:
fixes a::real
shows "Sup (insert a (insert b s)) = Sup (insert (max a b) s)"
--- a/src/HOL/Analysis/metricarith.ml Sun Oct 27 12:09:07 2019 -0400
+++ b/src/HOL/Analysis/metricarith.ml Sun Oct 27 12:13:04 2019 -0400
@@ -194,7 +194,7 @@
addsimps @{thms empty_iff insert_iff})))
val ball_simp =
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps
- @{thms Set.ball_simps(7) Set.ball_simps(5)})
+ @{thms Set.ball_empty ball_insert})
val dist_refl_sym_simp =
Simplifier.rewrite (put_simpset HOL_ss ctxt addsimps @{thms dist_commute dist_self})
val metric_eq_thm =