src/HOL/Dense_Linear_Order.thy
changeset 29372 df457e0d9a55
parent 29252 ea97aa6aeba2
child 29509 1ff0f3f08a7b