HomeIsabelle/Phabricator

Update KD_Tree entry to incorporate HOL-Analysis primites 'vec', 'dist' and…