src/HOL/Algebra/Coset.thy
changeset 24111 20e74aa5f56b
parent 23463 9953ff53cc64
child 26203 9625f3579b48