--- a/src/HOL/Integ/IntDef.ML Thu Jul 15 10:34:00 1999 +0200
+++ b/src/HOL/Integ/IntDef.ML Thu Jul 15 10:34:37 1999 +0200
@@ -149,13 +149,13 @@
Goalw [neg_def, int_def] "~ neg(int n)";
by (Simp_tac 1);
-qed "not_neg_nat";
+qed "not_neg_int";
Goalw [neg_def, int_def] "neg(- (int (Suc n)))";
by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "neg_zminus_nat";
+qed "neg_zminus_int";
-Addsimps [neg_zminus_nat, not_neg_nat];
+Addsimps [neg_zminus_int, not_neg_int];
(**** zadd: addition on Integ ****)
@@ -378,6 +378,10 @@
by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
qed "zdiff_zmult_distrib2";
+Goalw [int_def] "(int m) * (int n) = int (m * n)";
+by (simp_tac (simpset() addsimps [zmult]) 1);
+qed "zmult_int";
+
Goalw [int_def] "int 0 * z = int 0";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by (asm_simp_tac (simpset() addsimps [zmult]) 1);