--- a/src/HOL/Integ/IntDef.thy Thu Jun 16 18:25:54 2005 +0200
+++ b/src/HOL/Integ/IntDef.thy Thu Jun 16 19:51:04 2005 +0200
@@ -217,9 +217,12 @@
zadd_zmult_distrib zadd_zmult_distrib2
zdiff_zmult_distrib zdiff_zmult_distrib2
-lemma zmult_int: "(int m) * (int n) = int (m * n)"
+lemma int_mult: "int (m * n) = (int m) * (int n)"
by (simp add: int_def mult)
+text{*Compatibility binding*}
+lemmas zmult_int = int_mult [symmetric]
+
lemma zmult_1: "(1::int) * z = z"
by (cases z, simp add: One_int_def int_def mult)
@@ -442,7 +445,6 @@
lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
by (insert zless_nat_conj [of 0], auto)
-
lemma nat_add_distrib:
"[| (0::int) \<le> z; 0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
by (cases z, cases z', simp add: nat add le int_def Zero_int_def)