# HG changeset patch
# User immler
# Date 1572192784 14400
# Node ID 23e6eef4e6aa46a120c34105ca9f906657cb5ad3
# Parent  420359ba6acde48aa7e65af504f5b2f12dee4c11
avoid referring to lemmas by index

diff -r 420359ba6acd -r 23e6eef4e6aa src/HOL/Analysis/Metric_Arith.thy
--- 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)"
diff -r 420359ba6acd -r 23e6eef4e6aa src/HOL/Analysis/metricarith.ml
--- 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 =