[isabelle] SMT proof fails with exception


Dear list,

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.


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