src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
Sun, 25 Oct 2009 08:57:35 +0100 chaieb Add a quantifier elimination for parametric linear arithmetic over ordered fields (parameters are multivariate polynomials)
less more (0) tip