equal
deleted
inserted
replaced
176 apply(simp add: add_mult_distrib [symmetric]) |
176 apply(simp add: add_mult_distrib [symmetric]) |
177 done |
177 done |
178 |
178 |
179 lemma [quot_respect]: |
179 lemma [quot_respect]: |
180 shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw" |
180 shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw" |
181 apply(simp only: fun_rel.simps) |
181 apply(simp only: fun_rel_def) |
182 apply(rule allI | rule impI)+ |
182 apply(rule allI | rule impI)+ |
183 apply(rule equivp_transp[OF int_equivp]) |
183 apply(rule equivp_transp[OF int_equivp]) |
184 apply(rule mult_raw_fst) |
184 apply(rule mult_raw_fst) |
185 apply(assumption) |
185 apply(assumption) |
186 apply(rule mult_raw_snd) |
186 apply(rule mult_raw_snd) |