src/HOL/Algebra/Coset.thy
changeset 82314 c95eca07f6a0
parent 82248 e8c96013ea8a