# 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) \<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)