--- a/src/HOL/Library/FrechetDeriv.thy Fri Apr 30 13:31:32 2010 -0700
+++ b/src/HOL/Library/FrechetDeriv.thy Fri Apr 30 13:51:17 2010 -0700
@@ -54,11 +54,6 @@
subsection {* Addition *}
-lemma add_diff_add:
- fixes a b c d :: "'a::ab_group_add"
- shows "(a + c) - (b + d) = (a - b) + (c - d)"
-by simp
-
lemma bounded_linear_add:
assumes "bounded_linear f"
assumes "bounded_linear g"
@@ -402,11 +397,6 @@
subsection {* Inverse *}
-lemma inverse_diff_inverse:
- "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
-
lemmas bounded_linear_mult_const =
mult.bounded_linear_left [THEN bounded_linear_compose]