Re: [isabelle] jEdit apparantly proves False


you probably missed the relevant entry in the NEWS for Isabelle 2013-1:

*** Prover IDE -- Isabelle/Scala/jEdit ***
* Improved integration of HOL/Falso (see

Personally, I am delighted to see this finally happening, I'd say it's
about time. In fact, it may be the one thing that finally gets me to
abandon Proof General in favour of jEdit.


On 11/19/2013 01:40 PM, Peter Lammich wrote:
> Hi all,
> while giving a tutorial on Isabelle, I run into the following strange
> effect, where jEdit seems to indicate that a lemma is proven. Actually,
> the lemma just contains a diverging method invocation. See screenshot.
> To reproduce this behaviour, just load the attached theory file, wait a
> few seconds (the simp add: A A[symmetric] is marked purple now). Then
> move the cursor after the lemma and type some newlines, save the file,
> and you get (on my machine) the above effect. You can even use the lemma
> to prove further non-theorems from it without any problems!
> --
>   Peter
> p.s.
>   As I can see from some homework submissions, some of our students seem
> to run into this effect regularly when solving homeworks :(
> pps:
>  Thm.peek_status @{thm f} returns 
>   val it = {failed = true, oracle = false, unfinished = false}:
>    {failed: bool, oracle: bool, unfinished: bool}

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