src/HOL/Algebra/Sylow.thy
changeset 23719 ccd9cb15c062
parent 20318 0e0ea63fe768
child 25134 3d4953e88449