(* Title: HOL/Decision_Procs/Ferrack.thy Author: Amine Chaieb *) theory Ferrack imports Complex_Main Dense_Linear_Order DP_Library "HOL-Library.Code_Target_Numeral" begin section ‹Quantifier elimination for ‹ℝ (0, 1, +, <)›› (*********************************************************************************) (**** SHADOW SYNTAX AND SEMANTICS ****) (*********************************************************************************)