src/HOL/ex/Dense_Linear_Order_Ex.thy
changeset 24059 89a5382406a1
parent 23905 717a6cb1c659
child 26160 ff5bb2b532b3
equal deleted inserted replaced
24058:81aafd465662 24059:89a5382406a1