John Harrison: A HOL Theory of Euclidean Space. TPHOLs 2005: 114-129