src/HOL/Dense_Linear_Order.thy
changeset 25194 37a1743f0fc3
parent 25106 ff8fee9e752c
child 26040 08d52e2dba07
equal deleted inserted replaced
25193:e2e1a4b00de3 25194:37a1743f0fc3