src/HOL/Lex/Chopper.thy
changeset 2355 ee9bdbe2ac8a
parent 1559 9ba0906aa60d
child 2609 4370e5f0fa3f