src/HOL/Dense_Linear_Order.thy
changeset 27123 11fcdd5897dd
parent 26733 47224a933c14