[isabelle] Auto has to be invoked twice to succeed

Dear all,

I came across some interesting behavior with respect to the auto proof
method. In the attached theory, auto has to be applied twice in a row in
order to solve the goal. The first invocation solves the first subgoal and
transforms the second, with the second invocation solving what remains of
the second subgoal. So far, I was under the impression that when invoking
auto, it solves/transforms the subgoals until it cannot do anything else,
guaranteeing that a second invocation fails immediately. Any clues on what
is happening here?


Attachment: Scratch.thy
Description: Binary data

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