src/HOL/Dense_Linear_Order.thy
changeset 24669 4579eac2c997
parent 24640 85a6c200ecd3
child 24679 5b168969ffe0
equal deleted inserted replaced
24668:4058b7b0925c 24669:4579eac2c997