src/HOL/Real/RealVector.thy

 where
   "x /\<^sub>R r == scaleR (inverse r) x"
 
 end
 
-instance real :: scaleR
-  real_scaleR_def [simp]: "scaleR a x \<equiv> a * x" ..
+instantiation real :: scaleR
+begin
+
+definition
+  real_scaleR_def [simp]: "scaleR a x = a * x"
+
+instance ..
+
+end
 
 class real_vector = scaleR + ab_group_add +
   assumes scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
   and scaleR_left_distrib: "scaleR (a + b) x = scaleR a x + scaleR b x"
   and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"

 subsection {* Real normed vector spaces *}
 
 class norm = type +
   fixes norm :: "'a \<Rightarrow> real"
 
-instance real :: norm
-  real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
+instantiation real :: norm
+begin
+
+definition
+  real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>"
+
+instance ..
+
+end
 
 class sgn_div_norm = scaleR + norm + sgn +
   assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
 
 class real_normed_vector = real_vector + sgn_div_norm +