equal
deleted
inserted
replaced
106 apply(simp add: add_mult_distrib [symmetric]) |
106 apply(simp add: add_mult_distrib [symmetric]) |
107 done |
107 done |
108 |
108 |
109 lemma mult_raw_rsp[quot_respect]: |
109 lemma mult_raw_rsp[quot_respect]: |
110 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw" |
110 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw" |
111 apply(simp only: fun_rel.simps) |
111 apply(simp only: fun_rel_def) |
112 apply(rule allI | rule impI)+ |
112 apply(rule allI | rule impI)+ |
113 apply(rule equivp_transp[OF int_equivp]) |
113 apply(rule equivp_transp[OF int_equivp]) |
114 apply(rule mult_raw_fst) |
114 apply(rule mult_raw_fst) |
115 apply(assumption) |
115 apply(assumption) |
116 apply(rule mult_raw_snd) |
116 apply(rule mult_raw_snd) |