src/HOL/Multivariate_Analysis/Linear_Algebra.thy

--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -1507,6 +1507,8 @@
   show "linear f" ..
 qed
 
+lemmas linear_linear = linear_conv_bounded_linear[symmetric]
+
 lemma linear_bounded_pos:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes lf: "linear f"