[isabelle] linarith_split_limit_exceeded (current value is 9)



Hello,

In my formalisation I'm using various very simple algebraic calculations
as I do everything step by step
( adding up factors, expanding/ getting rid of - outside parentheses, showing equality of algebraic expressions etc etc.. )that I
would expect would be solved by linarith or simp or auto.

Very often, when I call Sledgehammer or try0 I keep getting
"Proof found"
and then repeatedly the message :
"
linarith_split_limit_exceeded (current value is 9)"

I can see this issue has been discussed before but I'm not sure how I could get rid of this problem.
Is there some setting/ macro/plugin I could change perhaps?

Many thanks in advance,
Angeliki




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