--- a/src/HOL/Integ/IntDef.ML Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Integ/IntDef.ML Fri Oct 05 21:52:39 2001 +0200
@@ -7,8 +7,8 @@
*)
-(*Rewrite the overloaded 0::int to (int 0)*)
-Addsimps [Zero_def];
+(*Rewrite the overloaded 0::int to (int 0)*) (* FIXME !? *)
+Addsimps [Zero_int_def];
Goalw [intrel_def] "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)";
by (Blast_tac 1);
@@ -326,7 +326,7 @@
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
qed "zmult_int0";
-Goalw [int_def] "int 1' * z = z";
+Goalw [int_def] "int (Suc 0) * z = z";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
qed "zmult_int1";
@@ -335,7 +335,7 @@
by (rtac ([zmult_commute, zmult_int0] MRS trans) 1);
qed "zmult_int0_right";
-Goal "z * int 1' = z";
+Goal "z * int (Suc 0) = z";
by (rtac ([zmult_commute, zmult_int1] MRS trans) 1);
qed "zmult_int1_right";