# HG changeset patch
# User wenzelm
# Date 1546785536 -3600
# Node ID 7cd977863194a87b0a532996d1cb0e8c3952c3e4
# Parent  157990515be16dcb272fa6f1f0c3caa8034a9857
retain important whitespace (see 1daf07b65385);

diff -r 157990515be1 -r 7cd977863194 src/HOL/Analysis/Operator_Norm.thy
--- 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)"