1.1 --- a/src/HOL/HOL.thy	Wed Jan 21 18:37:44 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Jan 21 23:40:23 2009 +0100
     1.3 @@ -208,34 +208,34 @@
     1.4  
     1.5  subsubsection {* Generic classes and algebraic operations *}
     1.6  
     1.7 -class default = type +
     1.8 +class default =
     1.9    fixes default :: 'a
    1.10  
    1.11 -class zero = type + 
    1.12 +class zero = 
    1.13    fixes zero :: 'a  ("0")
    1.14  
    1.15 -class one = type +
    1.16 +class one =
    1.17    fixes one  :: 'a  ("1")
    1.18  
    1.19  hide (open) const zero one
    1.20  
    1.21 -class plus = type +
    1.22 +class plus =
    1.23    fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
    1.24  
    1.25 -class minus = type +
    1.26 +class minus =
    1.27    fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
    1.28  
    1.29 -class uminus = type +
    1.30 +class uminus =
    1.31    fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
    1.32  
    1.33 -class times = type +
    1.34 +class times =
    1.35    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    1.36  
    1.37 -class inverse = type +
    1.38 +class inverse =
    1.39    fixes inverse :: "'a \<Rightarrow> 'a"
    1.40      and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    1.41  
    1.42 -class abs = type +
    1.43 +class abs =
    1.44    fixes abs :: "'a \<Rightarrow> 'a"
    1.45  begin
    1.46  
    1.47 @@ -247,10 +247,10 @@
    1.48  
    1.49  end
    1.50  
    1.51 -class sgn = type +
    1.52 +class sgn =
    1.53    fixes sgn :: "'a \<Rightarrow> 'a"
    1.54  
    1.55 -class ord = type +
    1.56 +class ord =
    1.57    fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.58      and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.59  begin
    1.60 @@ -1675,7 +1675,7 @@
    1.61  
    1.62  text {* Equality *}
    1.63  
    1.64 -class eq = type +
    1.65 +class eq =
    1.66    fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.67    assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
    1.68  begin