[isabelle] system of representatives of an equivalence relation

Dear fellow Isabellers,

I am wondering whether there is already a way in the Isabelle/HOL library (or the AFP, for that matter) to obtain a system of representatives (I'm not sure whether this is the correct term, in German it is called "Repräsentantensystem") for a given equivalence relation, i.e., a set containing one representative of each equivalence class?

thanks in advance and cheers


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