src/HOL/Dense_Linear_Order.thy
changeset 26819 56036226028b
parent 26733 47224a933c14