src/HOL/Analysis/Ordered_Euclidean_Space.thy
changeset 68743 91162dd89571
parent 68239 0764ee22a4d1
child 68833 fde093888c16