Re: [isabelle] SMT proof fails with exception

> I have a theorem on which I invoke Sledgehammer, but with "Try methods"
> disabled. Sledgehammer succeeds and suggests 'smt'. But if I click on
> the suggestion, I get:
>  exception THM 0 raised (line 89 of "goal.ML"):
> Again, I can provide a theory which reproduces the problem.

Please do so. Thanks.


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