src/HOL/LOrder.thy
changeset 14872 3f2144aebd76
parent 14738 83f1a514dcb4
child 15010 72fbe711e414