src/HOL/ex/LexOrds.thy
changeset 25517 36d710d1dbce
parent 22309 87ec1ca65312
child 27742 df552e6027cf