src/HOL/ex/LexOrds.thy
changeset 29156 89f76a58a378
parent 27742 df552e6027cf