src/HOL/Orderings.thy
changeset 32777 8ae3a48c69d9
parent 32215 87806301a813
child 32887 85e7ab9020ba