src/HOL/Algebra/Coset.thy
changeset 30056 0a35bee25c20
parent 29237 e90d9d51106b
child 30198 922f944f03b2