src/HOL/Lex/MaxChop.thy
changeset 7333 6cb15c6f1d9f
parent 6481 dbf2d9b3d6c8
child 8732 aef229ca5e77