--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Sep 01 22:32:58 2015 +0200
@@ -2178,7 +2178,7 @@
apply auto
done
-text \<open>Considering derivative @{typ "real \<Rightarrow> 'b\<Colon>real_normed_vector"} as a vector.\<close>
+text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"