src/HOL/HOL.thy
```     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
```