src/HOL/Library/Dense_Linear_Order.thy
changeset 27682 25aceefd4786
parent 27487 c8a6ce181805
child 27825 12254665fc41