[isabelle] Isabelle2016-1-RC1 sledgehammer "Try this: by presburger" fails
In Isabelle2016-1-RC1 I am seeing instances where sledgehammer
says, for example:
"cvc4": Try this: by presburger (24 ms)
"z3": Try this: by presburger (16 ms)
"spass": Try this: by presburger (20 ms)
But attempting to use "by presburger" fails.
In such cases, "by metis" succeeds.
I don't know if that is enough of a clue as to where to look.
I am not sure how to abstract an example of this. Is there
another way I can supply the necessary information?
- Gene Stark
This archive was generated by a fusion of
Pipermail (Mailman edition) and