src/HOL/ex/LexOrds.thy
changeset 23279 e39dd93161d9
parent 22309 87ec1ca65312
child 27742 df552e6027cf