doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML

--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Tue Mar 20 08:27:23 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Tue Mar 20 10:23:31 2007 +0100
@@ -17,28 +17,22 @@
 
 fun nat i = nat_aux Nat.Zero_nat i;
 
-fun op_eq_bit false false = true
-  | op_eq_bit true true = true
-  | op_eq_bit false true = false
-  | op_eq_bit true false = false;
-
 end; (*struct Integer*)
 
 structure Classes = 
 struct
 
-type 'a semigroup = {Classes__mult : 'a -> 'a -> 'a};
-fun mult (A_:'a semigroup) = #Classes__mult A_;
+type 'a semigroup = {mult : 'a -> 'a -> 'a};
+fun mult (A_:'a semigroup) = #mult A_;
 
 type 'a monoidl =
-  {Classes__monoidl_semigroup : 'a semigroup, Classes__neutral : 'a};
+  {Classes__monoidl_semigroup : 'a semigroup, neutral : 'a};
 fun monoidl_semigroup (A_:'a monoidl) = #Classes__monoidl_semigroup A_;
-fun neutral (A_:'a monoidl) = #Classes__neutral A_;
+fun neutral (A_:'a monoidl) = #neutral A_;
 
-type 'a group =
-  {Classes__group_monoidl : 'a monoidl, Classes__inverse : 'a -> 'a};
+type 'a group = {Classes__group_monoidl : 'a monoidl, inverse : 'a -> 'a};
 fun group_monoidl (A_:'a group) = #Classes__group_monoidl A_;
-fun inverse (A_:'a group) = #Classes__inverse A_;
+fun inverse (A_:'a group) = #inverse A_;
 
 fun inverse_int i = IntInf.~ i;
 
@@ -46,15 +40,14 @@
 
 fun mult_int i j = IntInf.+ (i, j);
 
-val semigroup_int = {Classes__mult = mult_int} : IntInf.int semigroup;
+val semigroup_int = {mult = mult_int} : IntInf.int semigroup;
 
 val monoidl_int =
-  {Classes__monoidl_semigroup = semigroup_int,
-    Classes__neutral = neutral_int}
-  : IntInf.int monoidl;
+  {Classes__monoidl_semigroup = semigroup_int, neutral = neutral_int} :
+  IntInf.int monoidl;
 
 val group_int =
-  {Classes__group_monoidl = monoidl_int, Classes__inverse = inverse_int} :
+  {Classes__group_monoidl = monoidl_int, inverse = inverse_int} :
   IntInf.int group;
 
 fun pow_nat A_ (Nat.Suc n) x =