[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?

 Julian

Attachment: Scratch.thy
Description: Binary data



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