1.1 --- a/src/HOL/Integ/IntDef.ML	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Integ/IntDef.ML	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -(*Rewrite the overloaded 0::int to (int 0)*)
     1.8 -Addsimps [Zero_def];
     1.9 +(*Rewrite the overloaded 0::int to (int 0)*)    (* FIXME !? *)
    1.10 +Addsimps [Zero_int_def];
    1.11  
    1.12  Goalw  [intrel_def] "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)";
    1.13  by (Blast_tac 1);
    1.14 @@ -326,7 +326,7 @@
    1.15  by (asm_simp_tac (simpset() addsimps [zmult]) 1);
    1.16  qed "zmult_int0";
    1.17  
    1.18 -Goalw [int_def] "int 1' * z = z";
    1.19 +Goalw [int_def] "int (Suc 0) * z = z";
    1.20  by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
    1.21  by (asm_simp_tac (simpset() addsimps [zmult]) 1);
    1.22  qed "zmult_int1";
    1.23 @@ -335,7 +335,7 @@
    1.24  by (rtac ([zmult_commute, zmult_int0] MRS trans) 1);
    1.25  qed "zmult_int0_right";
    1.26  
    1.27 -Goal "z * int 1' = z";
    1.28 +Goal "z * int (Suc 0) = z";
    1.29  by (rtac ([zmult_commute, zmult_int1] MRS trans) 1);
    1.30  qed "zmult_int1_right";
    1.31