# HG changeset patch # User bauerg # Date 962879257 -7200 # Node ID 8baf94ddb34532de8f728cf80e54a61d4fd8cd47 # Parent 879e0f0cd04703ba80db4eb580bc574b607bf4ba removed sorry; diff -r 879e0f0cd047 -r 8baf94ddb345 src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Jul 06 12:27:36 2000 +0200 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Jul 06 12:27:37 2000 +0200 @@ -162,7 +162,7 @@ proof (intro exI conjI) have "(x, h x) \ graph H'' h''" . also have "... \\ graph H' h'" . - finally have xh:"(x, h x) \ graph H' h'" . + finally have xh\ "(x, h x)\ graph H' h'" . thus x: "x\H'" .. show y: "y\H'" .. show "graph H' h' \\ graph H h" @@ -463,7 +463,7 @@ bounded by $p$. *} -lemma sup_norm_pres: +lemma sup_norm_pres\ "[| M = norm_pres_extensions E p F f; c\ chain M; graph H h = Union c |] ==> \ x\H. h x \\ p x" proof @@ -520,7 +520,7 @@ show ?L proof fix x assume "x\H" - show "!! a b :: real. [| - a \\ b; b \\ a |] ==> abs b \\ a" + show "!! a b \: real. [| - a \\ b; b \\ a |] ==> abs b \\ a" by arith show "- p x \\ h x" proof (rule real_minus_le)