src/HOL/Lex/Chopper.thy
changeset 8145 cdd5386eb6fe
parent 2609 4370e5f0fa3f
child 10338 291ce4c4b50e