doc-src/IsarAdvanced/Classes/Thy/Classes.thy
changeset 22473 753123c89d72
parent 22347 ddbf185a3be0
child 22479 de15ea8fb348
     1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Mon Mar 19 19:28:27 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Mar 20 08:27:15 2007 +0100
     1.3 @@ -161,7 +161,7 @@
     1.4    assumed to be associative:
     1.5  *}
     1.6  
     1.7 -    class semigroup =
     1.8 +    class semigroup = type +
     1.9        fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<^loc>\<otimes>" 70)
    1.10        assumes assoc: "(x \<^loc>\<otimes> y) \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
    1.11  
    1.12 @@ -333,7 +333,7 @@
    1.13    is nothing else than a locale:
    1.14  *}
    1.15  
    1.16 -class idem =
    1.17 +class idem = type +
    1.18    fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
    1.19    assumes idem: "f (f x) = f x"
    1.20