src/HOL/ex/Dense_Linear_Order_Ex.thy
changeset 29943 922b931fd2eb
parent 29823 0ab754d13ccd