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



Hi,

sometimes I get

   Successful attempt to solve goal by exported rule:

and

   goal:
  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.