src/HOL/Multivariate_Analysis/Derivative.thy

--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sun Oct 25 17:31:14 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Oct 26 23:41:27 2015 +0000
@@ -24,9 +24,6 @@
     by (rule netlimit_within [of a UNIV])
 qed simp
 
-(* Because I do not want to type this all the time *)
-lemmas linear_linear = linear_conv_bounded_linear[symmetric]
-
 declare has_derivative_bounded_linear[dest]
 
 subsection \<open>Derivatives\<close>