src/HOL/ex/Dense_Linear_Order_Ex.thy
changeset 28412 0608c04858c7
parent 26160 ff5bb2b532b3
child 29823 0ab754d13ccd
equal deleted inserted replaced
28411:93ec7fa3b3a0 28412:0608c04858c7