*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Handling failed proof*From*: Jeremy Dawson <jeremy at rsise.anu.edu.au>*Date*: Thu, 30 Sep 2010 11:24:54 +1000*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTikS1oojjFRqEFGKJPeK0cSQWj-jHk-PqC3PGG3d@mail.gmail.com>*References*: <AANLkTikS1oojjFRqEFGKJPeK0cSQWj-jHk-PqC3PGG3d@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.24 (X11/20100317)

John Munroe wrote:

Hi, I'm wondering why the exception handling in the following doesn't behave what I expected to. Does it not try to prove goal1, and if it fails, it tries to prove goal2? goal2 should be provable, but I still get a Proof failed exception. let val ctxt = @{context} val goal1 = @{prop "EX x y. x > y"} val goal2 = @{prop "EX (x::real) y. x > y"} in Goal.prove ctxt [] [] goal1 (fn _ => auto_tac (clasimpset_of ctxt)) handle THM _ => Goal.prove ctxt [] [] goal2 (fn _ => auto_tac (clasimpset_of ctxt)) end; Thank you for the help. John

John,

It can mean (1) the resulting lazy list of new proof states is empty (2) an ML exception is raised

I'd guess that this issue would explain the unexpected behaviour Jeremy

**Follow-Ups**:**Re: [isabelle] Handling failed proof***From:*John Munroe

**References**:**[isabelle] Handling failed proof***From:*John Munroe

- Previous by Date: [isabelle] Proving with Goal.prove
- Next by Date: Re: [isabelle] Handling failed proof
- Previous by Thread: Re: [isabelle] Handling failed proof
- Next by Thread: Re: [isabelle] Handling failed proof
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list