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:

and

  goal:
 No subgoals!

This means a certain fix-assume-show refinement has worked out.


but with

  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?


	Makarius





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