# HG changeset patch
# User huffman
# Date 1176313363 -7200
# Node ID c40465deaf2073d915bd3dab354bdc7cbc87d214
# Parent  d33735c0f22579b227457bcbe2ead3e89de1e9e3
new class syntax for scaleR and norm classes

diff -r d33735c0f225 -r c40465deaf20 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Wed Apr 11 09:40:29 2007 +0200
+++ b/src/HOL/Real/RealVector.thy	Wed Apr 11 19:42:43 2007 +0200
@@ -35,10 +35,11 @@
 
 subsection {* Real vector spaces *}
 
-axclass scaleR < type
+class scaleR = type +
+  fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a"
 
-consts
-  scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a::scaleR" (infixr "*#" 75)
+notation
+  scaleR (infixr "*#" 75)
 
 abbreviation
   divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a::scaleR" (infixl "'/#" 70) where
@@ -48,10 +49,8 @@
   scaleR (infixr "*\<^sub>R" 75) and
   divideR (infixl "'/\<^sub>R" 70)
 
-instance real :: scaleR ..
-
-defs (overloaded)
-  real_scaleR_def: "scaleR a x \<equiv> a * x"
+instance real :: scaleR
+  real_scaleR_def: "scaleR a x \<equiv> a * x" ..
 
 axclass real_vector < scaleR, ab_group_add
   scaleR_right_distrib: "scaleR a (x + y) = scaleR a x + scaleR a y"
@@ -362,13 +361,11 @@
 
 subsection {* Real normed vector spaces *}
 
-axclass norm < type
-consts norm :: "'a::norm \<Rightarrow> real"
+class norm = type +
+  fixes norm :: "'a \<Rightarrow> real"
 
-instance real :: norm ..
-
-defs (overloaded)
-  real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>"
+instance real :: norm
+  real_norm_def [simp]: "norm r \<equiv> \<bar>r\<bar>" ..
 
 axclass normed < plus, zero, norm
   norm_ge_zero [simp]: "0 \<le> norm x"