src/HOL/Dense_Linear_Order.thy
changeset 24261 dd31811bdf46
parent 24081 84a5a6267d60
child 24270 f53b7dab4426