[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.

Any opinions?



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.