src/HOL/Algebra/Coset.thy
changeset 58187 d2ddd401d74d
parent 57512 cc97b347b301
child 61382 efac889fccbc