equal
deleted
inserted
replaced
371 end |
371 end |
372 |
372 |
373 lemma permute_self: |
373 lemma permute_self: |
374 shows "p \<bullet> p = p" |
374 shows "p \<bullet> p = p" |
375 unfolding permute_perm_def |
375 unfolding permute_perm_def |
376 by (simp add: add_assoc) |
376 by (simp add: add.assoc) |
377 |
377 |
378 lemma pemute_minus_self: |
378 lemma pemute_minus_self: |
379 shows "- p \<bullet> p = p" |
379 shows "- p \<bullet> p = p" |
380 unfolding permute_perm_def |
380 unfolding permute_perm_def |
381 by (simp add: add_assoc) |
381 by (simp add: add.assoc) |
382 |
382 |
383 |
383 |
384 subsection {* Permutations for functions *} |
384 subsection {* Permutations for functions *} |
385 |
385 |
386 instantiation "fun" :: (pt, pt) pt |
386 instantiation "fun" :: (pt, pt) pt |