src/HOL/LOrder.thy
changeset 20223 89d2758ecddf
parent 17508 c84af7f39a6b
child 21213 c81f016883df