author bauerg Wed, 09 Aug 2000 17:10:41 +0200 changeset 9560 b87a6afe5881 parent 9559 1f99296758c2 child 9561 714ad541a133
tuned;
--- a/src/HOL/Real/HahnBanach/Aux.thy	Wed Aug 09 11:53:00 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Wed Aug 09 17:10:41 2000 +0200
@@ -103,7 +103,7 @@
thus ?thesis by simp
qed

-lemma real_mult_inv_right1: "x \<noteq> #0 ==> x*rinv(x) = #1"
+lemma real_mult_inv_right1: "x \<noteq> #0 ==> x * rinv(x) = #1"
by simp

lemma real_mult_inv_left1: "x \<noteq> #0 ==> rinv(x) * x = #1"
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Aug 09 11:53:00 2000 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Aug 09 17:10:41 2000 +0200
@@ -167,7 +167,7 @@
qed blast
def H' == "H + lin x'"
-- {* Define $H'$ as the direct sum of $H$ and the linear closure of $x'$. \skp *}
-        obtain xi where "\<forall>y \<in> H. - p (y + x') - h y <= xi
+        obtain xi where "\<forall>y \<in> H. - p (y + x') - h y <= xi
\<and> xi <= p (y + x') - h y"
-- {* Pick a real number $\xi$ that fulfills certain inequations; this will *}
-- {* be used to establish that $h'$ is a norm-preserving extension of $h$.
@@ -198,7 +198,7 @@
qed

def h' == "\<lambda>x. let (y,a) = SOME (y,a). x = y + a \<cdot> x' \<and> y \<in> H
-                       in (h y) + a * xi"
+                       in h y + a * xi"
-- {* Define the extension $h'$ of $h$ to $H'$ using $\xi$. \skp *}
show ?thesis
proof