[isabelle] Run simplifier without arithmetic splitting?
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and