We now have presburger as a stand-alone proof method. Possibly the other procedures could be bundled into that. There are times when it is definitely worth the wait.
Larry > On 1 Dec 2015, at 16:14, Amine Chaieb <am...@chaieb.org> wrote: > > At the time we decided against it due to the following: > > By design arith has to solve its goal or fail fast otherwise. Quantifier > Elimination is just the opposite of both, since its is in its general form > a conversion, and also due to very hard complexity costs (in particular > for this MIR theory) cannot generally fail fast. > > For the same reason we did not have presburger, or ferrack or the other > procedures (from my thesis) inside arith. > > Amine. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
