src/HOL/Dense_Linear_Order.thy
changeset 25789 c0506ac5b6b4
parent 25106 ff8fee9e752c
child 26040 08d52e2dba07