src/HOL/Orderings.thy
changeset 73255 7e2a9a8c2b85
parent 71851 34ecb540a079
child 73271 05a873f90655