# HG changeset patch
# User hoelzl
# Date 1398238320 -7200
# Node ID 18f50d5f84ef391163848e244d41e9782a6764b9
# Parent  b3a2dedcc9ec1434b64e7f40a65d4ffa18bcfe40
remove add_eq_zero_iff, it is replaced by add_nonneg_eq_0_iff; also removes it from the simpset

diff -r b3a2dedcc9ec -r 18f50d5f84ef src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Tue Apr 22 12:41:34 2014 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Wed Apr 23 09:32:00 2014 +0200
@@ -267,12 +267,6 @@
 definition dist_finmap where
   "dist P Q = Max (range (\<lambda>i. dist ((P)\<^sub>F i) ((Q)\<^sub>F i))) + (if domain P = domain Q then 0 else 1)"
 
-lemma add_eq_zero_iff[simp]:
-  fixes a b::real
-  assumes "a \<ge> 0" "b \<ge> 0"
-  shows "a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
-using assms by auto
-
 lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^sub>F ` S)"
   by (rule finite_subset[of _ "proj P ` (domain P \<inter> S \<union> {x})"]) auto
 
@@ -406,6 +400,7 @@
     by (auto intro: Max_in Max_eqI)
   show "dist P Q = 0 \<longleftrightarrow> P = Q"
     by (auto simp: finmap_eq_iff dist_finmap_def Max_ge_iff finite_proj_diag Max_eq_iff
+        add_nonneg_eq_0_iff
       intro!: Max_eqI image_eqI[where x=undefined])
 next
   fix P Q R::"'a \<Rightarrow>\<^sub>F 'b"