src/HOL/Dense_Linear_Order.thy
changeset 24632 779fc4fcbf8b
parent 24422 c0b5ff9e9e4d
child 24640 85a6c200ecd3