src/HOL/Lex/AutoMaxChop.thy
changeset 13145 59bc43b51aa2
parent 5184 9b8547a9496a
child 14428 bb2b0e10d9be