On the formal analysis of geometrical optics in HOL

Publication
International Workshop on Automated Deduction in Geometry