src/HOL/ex/Erdoes_Szekeres.thy
changeset 68953 89a12af9c330
parent 68484 59793df7f853
child 69597 ff784d5a5bfb
equal deleted inserted replaced
68952:7700142d6d25 68953:89a12af9c330