src/HOL/Algebra/Coset.thy
changeset 22871 9ffb43b19ec6
parent 21404 eb85850d3eb7
child 23350 50c5b0912a0c