src/HOL/Dense_Linear_Order.thy
changeset 26840 ec46381f149d
parent 26733 47224a933c14