doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs
changeset 24991 c6f5cc939c29
parent 24628 33137422d7fd
child 25200 f1d2e106f2fe
--- 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;