| changeset 9633 | a71a83253997 |
| parent 9509 | 0f3ee1f89ca8 |
| child 10228 | e653cb933293 |
--- a/src/HOL/Integ/IntArith.ML Thu Aug 17 10:42:57 2000 +0200 +++ b/src/HOL/Integ/IntArith.ML Thu Aug 17 11:55:47 2000 +0200 @@ -73,7 +73,8 @@ Goal "(m = m*(n::int)) = (n = #1 | m = #0)"; by Auto_tac; -by (stac (zmult_cancel1 RS sym) 1); +by (subgoal_tac "m*#1 = m*n" 1); +by (dtac (zmult_cancel1 RS iffD1) 1); by Auto_tac; qed "zmult_eq_self_iff";