src/HOL/Lex/Chopper.thy
changeset 13571 d76a798281f4
parent 10338 291ce4c4b50e
child 14428 bb2b0e10d9be