equal
deleted
inserted
replaced
209 |
209 |
210 interpretation perm_permute: permute permute_perm |
210 interpretation perm_permute: permute permute_perm |
211 apply default |
211 apply default |
212 unfolding permute_perm_def |
212 unfolding permute_perm_def |
213 apply simp |
213 apply simp |
214 apply (simp only: diff_conv_add_uminus minus_add add_assoc) |
214 apply (simp only: diff_conv_add_uminus minus_add add.assoc) |
215 done |
215 done |
216 |
216 |
217 text {*Permuting functions.*} |
217 text {*Permuting functions.*} |
218 locale fun_permute = |
218 locale fun_permute = |
219 dom: permute perm1 + ran: permute perm2 |
219 dom: permute perm1 + ran: permute perm2 |