src/HOL/Algebra/AbelCoset.thy
changeset 25231 1aa9c8f022d0
parent 23463 9953ff53cc64
child 26203 9625f3579b48