src/HOL/Analysis/Inner_Product.thy

   (@{const_name uniformity}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
 
 setup \<open>Sign.add_const_constraint
   (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
 
-class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
+class%important real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   assumes inner_commute: "inner x y = inner y x"
   and inner_add_left: "inner (x + y) z = inner x z + inner y z"
   and inner_scaleR_left [simp]: "inner (scaleR r x) y = r * (inner x y)"
   and inner_ge_zero [simp]: "0 \<le> inner x x"

   unfolding differentiable_def by (blast intro: has_derivative_inner)
 
 
 subsection \<open>Class instances\<close>
 
-instantiation real :: real_inner
+instantiation%important real :: real_inner
 begin
 
 definition inner_real_def [simp]: "inner = ( * )"
 
 instance

 lemma
   shows real_inner_1_left[simp]: "inner 1 x = x"
     and real_inner_1_right[simp]: "inner x 1 = x"
   by simp_all
 
-instantiation complex :: real_inner
+instantiation%important complex :: real_inner
 begin
 
 definition inner_complex_def:
   "inner x y = Re x * Re y + Im x * Im y"
 

 qed (auto intro: summable_of_real)
 
 
 subsection \<open>Gradient derivative\<close>
 
-definition
+definition%important
   gderiv ::
     "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
           ("(GDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
 where
   "GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"