src/HOL/Dense_Linear_Order.thy
changeset 25345 dd5b851f8ef0
parent 25106 ff8fee9e752c
child 26040 08d52e2dba07
equal deleted inserted replaced
25344:00c2179db769 25345:dd5b851f8ef0