Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Executable Permutations in AFP/Planarity_Certi...

Email Gateway (Aug 22 2022 at 13:02):

From: Manuel Eberl <eberlm@in.tum.de>
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?

Cheers,

Manuel

Last updated: Apr 24 2024 at 01:07 UTC