src/HOL/Lex/Chopper.thy
changeset 1868 836950047d85
parent 1559 9ba0906aa60d
child 2609 4370e5f0fa3f