Re: [isabelle] Auto has to be invoked twice to succeed



On 14.07.2015 17:45, Julian Brunner wrote:
> That was also Manuel's first idea when I told him about it. However, it
> doesn't seem to have any effect here, as even (auto 100 100) doesn't solve
> the goal. Also, my interest here is less about finding a convenient proof
> (auto+ does it just fine, after all), and more about figuring out what is
> going on.

auto is designed such that it is usually idempotent, but without
guarantees. It calls first the simplifier and then safe, before trying
some classical reasoning. Sometimes, the simplifier needs a call to safe
first.




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