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.

Larry

> On 14 Aug 2016, at 11:28, Sascha BÃhme <boehmes at in.tum.de> 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.