src/HOL/Dense_Linear_Order.thy
changeset 26310 f8a7fac36e13
parent 26040 08d52e2dba07
child 26733 47224a933c14