src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 78178 a177f71dc79f
parent 77935 7f240b0dabd9
child 78200 264f2b69d09c