src/HOL/Lex/MaxChop.thy
changeset 12913 5ac498bffb6b
parent 8732 aef229ca5e77
child 14428 bb2b0e10d9be