But couldn’t these procedures be included in linarith, or at least in “try”? Larry
> On 13 Nov 2015, at 16:18, Tobias Nipkow <nip...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
