Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Real/HahnBanach/FunctionNorm.thy
changeset 9969 4753185f1dd2
parent 9503 3324cbbecef8
child 9998 09bf8fcd1c6e 
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Sep 15 12:39:57 2000 +0200
@@ -97,7 +97,7 @@
   "[| is_normed_vectorspace V norm; is_continuous V norm f|]
      ==> is_function_norm f V norm \<parallel>f\<parallel>V,norm" 
 proof (unfold function_norm_def is_function_norm_def 
-  is_continuous_def Sup_def, elim conjE, rule selectI2EX)
+  is_continuous_def Sup_def, elim conjE, rule someI2EX)
   assume "is_normed_vectorspace V norm"
   assume "is_linearform V f" 
   and e: "\<exists>c. \<forall>x \<in> V. |f x| <= c * norm x"
isabelle