author bauerg Thu, 06 Jul 2000 12:27:37 +0200 changeset 9262 8baf94ddb345 parent 9261 879e0f0cd047 child 9263 53e09e592278
removed sorry;
```--- 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) \<in> graph H'' h''" .
also have "... \\<subseteq> graph H' h'" .
-        finally have xh:"(x, h x) \<in> graph H' h'" .
+        finally have xh\<in> "(x, h x)\<in> graph H' h'" .
thus x: "x\<in>H'" ..
show y: "y\<in>H'" ..
show "graph H' h' \\<subseteq> graph H h"
@@ -463,7 +463,7 @@
bounded by \$p\$.
*}

-lemma sup_norm_pres:
+lemma sup_norm_pres\<in>
"[| M = norm_pres_extensions E p F f; c\<in> chain M;
graph H h = Union c |] ==> \<forall> x\<in>H. h x \\<le> p x"
proof
@@ -520,7 +520,7 @@
show ?L
proof
fix x assume "x\<in>H"
-      show "!! a b :: real. [| - a \\<le> b; b \\<le> a |] ==> abs b \\<le> a"
+      show "!! a b \<in>: real. [| - a \\<le> b; b \\<le> a |] ==> abs b \\<le> a"
by arith
show "- p x \\<le> h x"
proof (rule real_minus_le)```