diff -r b924fac38eec -r c6f5cc939c29 doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs --- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Thu Oct 11 23:03:51 2007 +0200 +++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs Fri Oct 12 08:20:43 2007 +0200 @@ -20,7 +20,10 @@ neutral :: a; }; -class (Classes.Monoidl a) => Group a where { +class (Classes.Monoidl a) => Monoid a where { +}; + +class (Classes.Monoid a) => Group a where { inverse :: a -> a; }; @@ -41,11 +44,14 @@ neutral = Classes.neutral_int; }; +instance Classes.Monoid Integer where { +}; + instance Classes.Group Integer where { inverse = Classes.inverse_int; }; -pow_nat :: (Classes.Group b) => Classes.Nat -> b -> b; +pow_nat :: (Classes.Monoid a) => Classes.Nat -> a -> a; pow_nat (Classes.Suc n) x = Classes.mult x (Classes.pow_nat n x); pow_nat Classes.Zero_nat x = Classes.neutral;