--- 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;