equal
deleted
inserted
replaced
55 (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2); |
55 (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2); |
56 by (etac (nat_0_le RS subst) 1); |
56 by (etac (nat_0_le RS subst) 1); |
57 by (Simp_tac 1); |
57 by (Simp_tac 1); |
58 qed "nat_less_iff"; |
58 qed "nat_less_iff"; |
59 |
59 |
60 Goal "(int m = z) = (m = nat z & #0 \\<le> z)"; |
60 Goal "(int m = z) = (m = nat z & #0 <= z)"; |
61 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff2])); |
61 by (auto_tac (claset(), simpset() addsimps [nat_eq_iff2])); |
62 qed "int_eq_iff"; |
62 qed "int_eq_iff"; |
63 |
63 |
64 Addsimps [inst "z" "number_of ?v" int_eq_iff]; |
64 Addsimps [inst "z" "number_of ?v" int_eq_iff]; |
65 |
65 |