src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 68000 40b790c5a11d
parent 67981 349c639e593c
child 68120 2f161c6910f7