[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 MHonArc.