src/HOL/Algebra/Coset.thy
changeset 23512 770e7f9f715b
parent 23463 9953ff53cc64
child 26203 9625f3579b48