src/HOL/Lex/Chopper.thy
changeset 13145 59bc43b51aa2
parent 10338 291ce4c4b50e
child 14428 bb2b0e10d9be