src/HOL/Lex/Chopper.thy
changeset 2250 891eb76b8045
parent 1559 9ba0906aa60d
child 2609 4370e5f0fa3f