src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 66294 0442b3f45556
parent 64758 3b33d2fc5fc0
child 66453 cc19f7ca2ed6