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â:
using this:
  âYs::form list.    Ys    cfâ (C::form)     
goal (1 subgoal):
 1. âYs::form list.    Ys    cfâ A â C     
variables:
  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.

- Gergely 


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