equal
deleted
inserted
replaced
71 |
71 |
72 (*** Products and 1, by T. M. Rasmussen ***) |
72 (*** Products and 1, by T. M. Rasmussen ***) |
73 |
73 |
74 Goal "(m = m*(n::int)) = (n = #1 | m = #0)"; |
74 Goal "(m = m*(n::int)) = (n = #1 | m = #0)"; |
75 by Auto_tac; |
75 by Auto_tac; |
76 by (stac (zmult_cancel1 RS sym) 1); |
76 by (subgoal_tac "m*#1 = m*n" 1); |
|
77 by (dtac (zmult_cancel1 RS iffD1) 1); |
77 by Auto_tac; |
78 by Auto_tac; |
78 qed "zmult_eq_self_iff"; |
79 qed "zmult_eq_self_iff"; |
79 |
80 |
80 Goal "[| #1 < m; #1 < n |] ==> #1 < m*(n::int)"; |
81 Goal "[| #1 < m; #1 < n |] ==> #1 < m*(n::int)"; |
81 by (res_inst_tac [("z2.0","#1*n")] zless_trans 1); |
82 by (res_inst_tac [("z2.0","#1*n")] zless_trans 1); |