src/HOL/Algebra/Coset.thy
changeset 16200 447c06881fbb
parent 15120 f0359f75682e
child 16417 9bc16273c2d4