Re: [isabelle] Issue with smt and linear arithmetic

This precise sort of thing has always annoyed me. I was under the impression that we could perform such simplifications (when there is a gcd; simply distributing the /2 is trivial), but upon looking, it seems that no such simprocs ever existed.


> On 14 Aug 2016, at 11:28, Sascha BÃhme <boehmes at> wrote:
> In your particular case, the obvious simplification for â(2x +2y) / 2â is not performed, because some rule or simproc is missing in linarithâs simpset. Extending the simpset appropriately would be a solution. Iâll see what I can do, such that your issue is resolved in the next release of Isabelle.

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