src/HOL/Algebra/Coset.thy
changeset 27885 76b51cd0a37c
parent 27717 21bbd410ba04
child 29237 e90d9d51106b