src/HOL/Lex/MaxChop.thy
changeset 5253 82a5ca6290aa
parent 4714 bcdf68c78e18
child 6481 dbf2d9b3d6c8