src/HOL/ex/Erdoes_Szekeres.thy
changeset 62390 842917225d56
parent 61343 5b5656a63bd6
child 63040 eb4ddd18d635
equal deleted inserted replaced
62380:29800666e526 62390:842917225d56