src/HOL/ex/Erdoes_Szekeres.thy
changeset 78659 b5f3d1051b13
parent 71472 c213d067e60f