src/HOL/ex/LexOrds.thy
changeset 23277 aa158e145ea3
parent 22309 87ec1ca65312
child 27742 df552e6027cf