A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL by Katherine Kosaian, Yong Kiam Tan and André Platzer Dec 15