[isabelle] Run simplifier without arithmetic splitting?



Hi,

I have the suspicion that the simplifier gets unbearably slow due to
excessive splitting by the built-in linarith procedure.

Is there any way to switch this off, or to reduce the split-limit, such
that I can test my hypothesis?

Reducing linarith_split_limit will bomb the trace output with messages,
which makes the whole thing even slower.

Thanks in advance for any help,
  Peter





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