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.
retain important whitespace (see 1daf07b65385);
authorwenzelm
Sun, 06 Jan 2019 15:38:56 +0100
changeset 69607 7cd977863194
parent 69606 157990515be1
child 69608 2b3a247889f8
retain important whitespace (see 1daf07b65385);
src/HOL/Analysis/Operator_Norm.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Analysis/Operator_Norm.thy	Sun Jan 06 15:11:13 2019 +0100
+++ b/src/HOL/Analysis/Operator_Norm.thy	Sun Jan 06 15:38:56 2019 +0100
@@ -11,6 +11,7 @@
 
 text \<open>This formulation yields zero if \<open>'a\<close> is the trivial vector space.\<close>
 
+text%important \<open>%whitespace\<close>
 definition%important
 onorm :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> real" where
 "onorm f = (SUP x. norm (f x) / norm x)"
isabelle