1.1 --- a/src/HOL/ex/Classpackage.thy	Mon Mar 19 19:28:27 2007 +0100
     1.2 +++ b/src/HOL/ex/Classpackage.thy	Tue Mar 20 08:27:15 2007 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -class semigroup =
     1.8 +class semigroup = type +
     1.9    fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70)
    1.10    assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
    1.11