[isabelle-dev] MIR decision procedure

[Lawrence Paulson]

But couldn’t these procedures be included in linarith, or at least in “try”?
Larry

> On 13 Nov 2015, at 16:18, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> MIR is "documented" in Amine's IJCAR 2006 paper "Verifying Mixed Real-Integer Quantifier Elimination". Maybe the title gives you a hint what it is good for. Ferrack stands for Ferrante & Rackoff, who invented this QE algorithm. This one may only be "documented" in Amine's PhD.