| changeset 10451 | 226d474e644d |
| parent 9544 | f9202e219a29 |
| child 10472 | 6569febd98e5 |
--- a/src/HOL/Integ/IntDef.ML Fri Nov 10 19:18:14 2000 +0100 +++ b/src/HOL/Integ/IntDef.ML Fri Nov 10 19:18:37 2000 +0100 @@ -319,6 +319,9 @@ by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1); qed "zdiff_zmult_distrib2"; +bind_thms ("int_distrib", + [zadd_zmult_distrib, zadd_zmult_distrib2, zdiff_zmult_distrib, zdiff_zmult_distrib2]); + Goalw [int_def] "(int m) * (int n) = int (m * n)"; by (simp_tac (simpset() addsimps [zmult]) 1); qed "zmult_int";