Re: [isabelle] successful attempt vs failed to apply initial proof method
On Thu, 17 Mar 2016, Buday Gergely wrote:
sometimes I get
Successful attempt to solve goal by exported rule:
This means a certain fix-assume-show refinement has worked out.
Failed to apply initial proof method
and Isabelle/Jedit does not accept the proof.
This means that proof method application has failed, e.g. a "by method"
step for the proof of "show" above.
and why the system says No subgoals! when despite of this it does not
accept the proof?
The message stems from really ancient time where there was a linear,
unstructured goal state.
In Isabelle2016 the default split into Output vs. State panel should make
the situation a bit clearer. Did you use that default? Or did you switch
back to the old way?
This archive was generated by a fusion of
Pipermail (Mailman edition) and