src/HOL/Dense_Linear_Order.thy
changeset 24085 cbad32e7ab40
parent 24081 84a5a6267d60
child 24270 f53b7dab4426
equal deleted inserted replaced
24084:d126c1fe64ed 24085:cbad32e7ab40