src/HOL/ex/Dense_Linear_Order_Ex.thy
changeset 30424 692279df7cc2
parent 29823 0ab754d13ccd
equal deleted inserted replaced
30423:6baef860dfa6 30424:692279df7cc2