src/HOL/Dense_Linear_Order.thy
changeset 24085 cbad32e7ab40
parent 24081 84a5a6267d60
child 24270 f53b7dab4426