src/HOL/Lex/Chopper.thy
changeset 13117 0b233f430076
parent 10338 291ce4c4b50e
child 14428 bb2b0e10d9be