src/HOL/Dense_Linear_Order.thy
changeset 29457 2eadbc24de8c
parent 29252 ea97aa6aeba2
child 29509 1ff0f3f08a7b