[isabelle] Executable Permutations in AFP/Planarity_Certificates
There is some very useful material on executable permutations (e.g.
defining permutations by their cycles) in the "Planarity_Certificates"
AFP entry. I need this material for my work on Social Choice Theory and
I think it is of great interest in general.
I suggest we move this material to an AFP entry of its own, or perhaps
even to HOL-Library.
This archive was generated by a fusion of
Pipermail (Mailman edition) and