| changeset 16733 | 236dfafbeb63 |
| parent 16642 | 849ec3962b55 |
| child 16770 | 1f1b1fae30e4 |
--- a/src/HOL/Integ/IntDef.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/Integ/IntDef.thy Thu Jul 07 12:39:17 2005 +0200 @@ -181,7 +181,7 @@ apply (simp add: congruent_def mult_ac) apply (rename_tac u v w x y z) apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z") -apply (simp add: mult_ac, arith) +apply (simp add: mult_ac) apply (simp add: add_mult_distrib [symmetric]) done