Re: [isabelle] successful attempt vs failed to apply initial proof method
> From: Makarius [mailto:makarius at sketis.net]
> On Thu, 17 Mar 2016, Buday Gergely wrote:
> 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?
I used Proof state, yes. Switching it off I see
show âYs::form list. Ys cfâ (A::form) â (C::form)
Successful attempt to solve goal by exported rule:
( (?A2::form) # (?Xsa2::form list) â (?C2::form) ) â
(âYs::form list. Ys cfâ ?C2 ) â âYs::form list. Ys cfâ ?A2 â ?C2
Failed to apply initial proof methodâ:
âYs::form list. Ys cfâ (C::form)
goal (1 subgoal):
1. âYs::form list. Ys cfâ A â C
A, C :: form
Is the above "exported rule" a fact, and, where does it come from? Can I use it to prove the goal, or it is a hypothetical fact that would prove the goal?
And, is there a reference of Output and State messages? The Isabelle/jEdit manual does not seem to contain one.
This archive was generated by a fusion of
Pipermail (Mailman edition) and