src/HOL/Dense_Linear_Order.thy
changeset 24465 70f0214b3ecc
parent 24422 c0b5ff9e9e4d
child 24640 85a6c200ecd3