equal
deleted
inserted
replaced
179 apply (rule equiv_intrel [THEN congruent2_commuteI]) |
179 apply (rule equiv_intrel [THEN congruent2_commuteI]) |
180 apply (force simp add: mult_ac, clarify) |
180 apply (force simp add: mult_ac, clarify) |
181 apply (simp add: congruent_def mult_ac) |
181 apply (simp add: congruent_def mult_ac) |
182 apply (rename_tac u v w x y z) |
182 apply (rename_tac u v w x y z) |
183 apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z") |
183 apply (subgoal_tac "u*y + x*y = w*y + v*y & u*z + x*z = w*z + v*z") |
184 apply (simp add: mult_ac, arith) |
184 apply (simp add: mult_ac) |
185 apply (simp add: add_mult_distrib [symmetric]) |
185 apply (simp add: add_mult_distrib [symmetric]) |
186 done |
186 done |
187 |
187 |
188 |
188 |
189 lemma mult: |
189 lemma mult: |