src/HOL/Lex/MaxChop.thy
changeset 8039 a901bafe4578
parent 6481 dbf2d9b3d6c8
child 8732 aef229ca5e77