src/HOL/Algebra/Coset.thy
changeset 77775 3cc55085d490
parent 77407 02af8a1b97f6
child 80067 c40bdfc84640