src/HOL/Orderings.thy
changeset 70537 17160e0a60b6
parent 69815 56d5bb8c102e
child 70749 5d06b7bb9d22