Re: [isabelle] jEdit apparantly proves False



Hallo,

I just wanted to add that I migrated to Isabelle/JEdit recently (with
Isabelle 2013-1) and I was rather confused by this behaviour, too.

Regards,
Christoph Feller

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.