[isabelle] successful attempt vs failed to apply initial proof method


sometimes I get

   Successful attempt to solve goal by exported rule:


  No subgoals!

but with

   Failed to apply initial proof method

and Isabelle/Jedit does not accept the proof. Where does it get the formula referred as "exported rule" from 

and why the system says No subgoals! when despite of this it does not accept the proof?

- Gergely

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