Re: [isabelle] arith tactic



> My understanding is that the arith tactic is able to handle the mod
> operator, provided that its second argument is a constant.

In principle, yes. In your case the resulting Presburger goal killed the
decision procedure. We are working on it but it may take a little while.
There is no doubt that this is an important class of formulae.

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.