src/HOL/Lex/Chopper.thy
changeset 2183 8d42a7bccf0b
parent 1559 9ba0906aa60d
child 2609 4370e5f0fa3f