src/HOL/Lex/MaxChop.thy
changeset 8364 0eb9ee70c8f8
parent 6481 dbf2d9b3d6c8
child 8732 aef229ca5e77