src/HOL/Real/RealVector.thy

 
 
 subsection {* Real vector spaces *}
 
 class scaleR = type +
-  fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a"
-
-notation
-  scaleR (infixr "*#" 75)
+  fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<^loc>*#" 75)
+begin
 
 abbreviation
-  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a::scaleR" (infixl "'/#" 70) where
+  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "\<^loc>'/#" 70)
+where
+  "x \<^loc>/# r == scaleR (inverse r) x"
+
+end
+
+abbreviation
+  divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a\<Colon>scaleR" (infixl "'/#" 70)
+where
   "x /# r == scaleR (inverse r) x"
 
 notation (xsymbols)
   scaleR (infixr "*\<^sub>R" 75) and
   divideR (infixl "'/\<^sub>R" 70)

 
 instance real :: norm
   real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
 
 class sgn_div_norm = scaleR + norm + sgn +
-  assumes sgn_div_norm: "sgn x = x /# norm x"
+  assumes sgn_div_norm: "sgn x = x \<^loc>/# norm x"
 
 class real_normed_vector = real_vector + sgn_div_norm +
   assumes norm_ge_zero [simp]: "0 \<le> norm x"
   and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = \<^loc>0"
   and norm_triangle_ineq: "norm (x \<^loc>+ y) \<le> norm x + norm y"