# HG changeset patch
# User wenzelm
# Date 947101777 -3600
# Node ID ce4bb031d664b068a580b992a0b862592a0e4400
# Parent  284d6a3c8bd2b5fc22146816aae48ab8faeff8bb
oops';

diff -r 284d6a3c8bd2 -r ce4bb031d664 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Jan 05 20:47:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Wed Jan 05 20:49:37 2000 +0100
@@ -786,7 +786,7 @@
           fix x; assume "x : F"; 
           from a; have "g x = f x"; ..;
           hence "rabs (f x) = rabs (g x)"; by simp;
-          also; from g_cont;
+          also; from _ _ g_cont;
           have "... <= function_norm E norm g * norm x";
           proof (rule norm_fx_le_norm_f_norm_x);
             show "x:E"; ..;