--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri May 07 12:16:57 2004 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Fri May 07 12:47:44 2004 +0200
@@ -5,7 +5,7 @@
header {* Extending non-maximal functions *}
-theory HahnBanachExtLemmas = FunctionNorm + RealLemmas:
+theory HahnBanachExtLemmas = FunctionNorm:
text {*
In this section the following context is presumed. Let @{text E} be
@@ -227,7 +227,7 @@
also have "\<dots> =
- a * (p (inverse a \<cdot> y + x0)) - a * (h (inverse a \<cdot> y))"
- by (rule real_mult_diff_distrib)
+ by (simp add: right_diff_distrib)
also from lz x0 y' have "- a * (p (inverse a \<cdot> y + x0)) =
p (a \<cdot> (inverse a \<cdot> y + x0))"
by (simp add: abs_homogenous abs_minus_eqI2)
@@ -247,7 +247,7 @@
a * (p (inverse a \<cdot> y + x0) - h (inverse a \<cdot> y))"
by simp
also have "... = a * p (inverse a \<cdot> y + x0) - a * h (inverse a \<cdot> y)"
- by (rule real_mult_diff_distrib2)
+ by (simp add: right_diff_distrib)
also from gz x0 y'
have "a * p (inverse a \<cdot> y + x0) = p (a \<cdot> (inverse a \<cdot> y + x0))"
by (simp add: abs_homogenous abs_eqI2)
--- a/src/HOL/Real/HahnBanach/RealLemmas.thy Fri May 07 12:16:57 2004 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: HOL/Real/HahnBanach/RealLemmas.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* Auxiliary theorems *}
-
-theory RealLemmas = Real:
-
-lemma real_mult_diff_distrib:
- "a * (- x - (y::real)) = - a * x - a * y"
-proof -
- have "- x - y = - x + - y" by simp
- also have "a * ... = a * - x + a * - y"
- by (simp only: right_distrib)
- also have "... = - a * x - a * y"
- by simp
- finally show ?thesis .
-qed
-
-lemma real_mult_diff_distrib2:
- "a * (x - (y::real)) = a * x - a * y"
-proof -
- have "x - y = x + - y" by simp
- also have "a * ... = a * x + a * - y"
- by (simp only: right_distrib)
- also have "... = a * x - a * y"
- by simp
- finally show ?thesis .
-qed
-
-end