[isabelle] isar in jedit : strange behavior



I am beginner in Isabelle and I try to understand isar. I have written the following proof in jedit

1 lemma  trivial2 : "p â (q â p)"
2 proof
3   assume p: "p"
4  then show "q â p"
5  proof
6   assume q:"q"
7   show "p" by assumption
8 qed
9 qed

On the line 6 I read in output panel :

    goal : No subgoals

But on line 6, I have still a goal (who can't be refined)

On the line 7, with cursor after show I read in output panel :

    goal : No subgoals

    Failed to refine any pending goal

But on this line, I have the goal "p" which is solved by not still discharged assumption p


--
courriel : michel.levy2009 at laposte.net
membres-liglab.imag.fr/michel.levy <http://membres-liglab.imag.fr/michel.levy>



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