src/HOL/Dense_Linear_Order.thy
changeset 26113 ba5909699cc3
parent 26040 08d52e2dba07
child 26733 47224a933c14