src/HOL/Library/Dense_Linear_Order.thy
changeset 29251 8f84a608883d
parent 29229 6f6262027054