# HG changeset patch
# User bauerg
# Date 1083926864 -7200
# Node ID 521aa281808a8e11bd08f332ac3970cf5e354544
# Parent  247615bfffb86c9ee5a77be58d51c4b2ec046807
*** empty log message ***

diff -r 247615bfffb8 -r 521aa281808a src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
--- 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)
diff -r 247615bfffb8 -r 521aa281808a src/HOL/Real/HahnBanach/RealLemmas.thy
--- 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