# 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);