src/HOL/Lex/MaxChop.ML
changeset 5901 a8e1ca1b2ec6
parent 5184 9b8547a9496a
child 6540 eaf90f6806df