Re: [isabelle] Handling failed proof



John Munroe wrote:
I'm wondering why the exception handling in the following doesn't
behave what I expected to.

  Goal.prove ctxt [] [] goal1
   (fn _ => auto_tac (clasimpset_of ctxt))
   handle THM _ =>
[...]

The Goal module catches the internal THM exception itself and re-raises it as a user error (exception ERROR). So the "handle THM _" does not catch it...

Alex





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