| changeset 59807 | 22bc39064290 |
| parent 58874 | 7172c7ffb047 |
| child 61799 | 4cf66f21b764 |
| 59806:d3d4ec6c21ef | 59807:22bc39064290 |
|---|---|
192 apply (fold eq_norm') |
192 apply (fold eq_norm') |
193 apply safe |
193 apply safe |
194 prefer 2 |
194 prefer 2 |
195 apply (simp add: comp_assoc) |
195 apply (simp add: comp_assoc) |
196 apply (rule ext) |
196 apply (rule ext) |
197 apply (drule_tac f="?a o ?b" in fun_cong) |
197 apply (drule_tac f="a o b" for a b in fun_cong) |
198 apply simp |
198 apply simp |
199 done |
199 done |
200 |
200 |
201 lemma fns: |
201 lemma fns: |
202 "fr o norm = norm o fr ==> |
202 "fr o norm = norm o fr ==> |