src/HOL/Orderings.thy
changeset 25246 584d8f2e1fc9
parent 25207 d58c14280367
child 25377 dcde128c84a2