Re: [isabelle] Handling failed proof



> Without addressing your specific example closely,  I can just point out that
> to talk of a tactic application "failing" (as the documentation does) is
> potentially ambiguous.
>
> It  can mean
> (1) the resulting lazy list of new proof states is empty
> (2) an ML exception is raised
>
> Needless to say one sort of failure can (and no doubt there are examples in
> the code) can be converted to the other
>
> I'd guess that this issue would explain the unexpected behaviour
>

Handling ERROR instead solves my problem. Thanks!

John

> Jeremy
>
>
>





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