equal
deleted
inserted
replaced
108 apply (simp_all add: o_assoc [symmetric]) |
108 apply (simp_all add: o_assoc [symmetric]) |
109 apply (simp_all add: o_assoc) |
109 apply (simp_all add: o_assoc) |
110 done |
110 done |
111 |
111 |
112 lemma fn_comm_power: |
112 lemma fn_comm_power: |
113 "fa o tr = tr o fr ==> fa ^ n o tr = tr o fr ^ n" |
113 "fa o tr = tr o fr ==> fa o^ n o tr = tr o fr o^ n" |
114 apply (rule ext) |
114 apply (rule ext) |
115 apply (induct n) |
115 apply (induct n) |
116 apply (auto dest: fun_cong) |
116 apply (auto dest: fun_cong) |
117 done |
117 done |
118 |
118 |