src/HOL/Lex/Chopper.thy
changeset 13049 ce180e5b7fa0
parent 10338 291ce4c4b50e
child 14428 bb2b0e10d9be