Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
oops';
authorwenzelm
Wed, 05 Jan 2000 20:49:37 +0100
changeset 8108 ce4bb031d664
parent 8107 284d6a3c8bd2
child 8109 aca11f954993
oops';
src/HOL/Real/HahnBanach/HahnBanach.thy file | annotate | diff | comparison | revisions 
--- 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"; ..;
isabelle