src/HOL/Algebra/Coset.thy
changeset 69766 76fbd806ebc5
parent 69749 10e48c47a549
child 69895 6b03a8cf092d