src/HOL/Algebra/Coset.thy
changeset 81640 c734c2a15e32
parent 81438 95c9af7483b1
child 82248 e8c96013ea8a