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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and