# HG changeset patch
# User paulson
# Date 932027677 -7200
# Node ID 63120b6dca501119d1e6f7fdabe41ea5081d0556
# Parent  d6a721e7125df0c220df7867e1891abc23c9d183
more renaming of theorems from _nat to _int (corresponding to a function that
was similarly renamed some time ago

Also new theorem zmult_int

diff -r d6a721e7125d -r 63120b6dca50 src/HOL/Integ/IntDef.ML
--- 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);