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