| changeset 8785 | 00cff9d083df |
| parent 8442 | 96023903c2df |
| child 9436 | 62bb04ab4b01 |
--- a/src/HOL/Integ/Int.ML Wed May 03 18:30:29 2000 +0200 +++ b/src/HOL/Integ/Int.ML Wed May 03 18:33:28 2000 +0200 @@ -69,6 +69,11 @@ (*** misc ***) +Goal "- (z - y) = y - (z::int)"; +by (Simp_tac 1); +qed "zminus_zdiff_eq"; +Addsimps [zminus_zdiff_eq]; + Goal "(w<z) = neg(w-z)"; by (simp_tac (simpset() addsimps [zless_def]) 1); qed "zless_eq_neg";