Virtual_Substitution Dependents

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

by Katherine Kosaian, Yong Kiam Tan and André Platzer