src/HOL/Orderings.thy
changeset 73428 9d1b5c0bdec8
parent 73411 1f1366966296
child 73526 a3cc9fa1295d