src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
changeset 62102 877463945ce9
parent 62101 26c0a70f78a3
child 62127 d8e7738bd2e9
     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Fri Jan 08 17:40:59 2016 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Fri Jan 08 17:41:04 2016 +0100
     1.3 @@ -152,6 +152,8 @@
     1.4  
     1.5  end
     1.6  
     1.7 +declare uniformity_Abort[where 'a="('a :: real_normed_vector) \<Rightarrow>\<^sub>L ('b :: real_normed_vector)", code]
     1.8 +
     1.9  lemma norm_blinfun_eqI:
    1.10    assumes "n \<le> norm (blinfun_apply f x) / norm x"
    1.11    assumes "\<And>x. norm (blinfun_apply f x) \<le> n * norm x"