Re: [isabelle] Run simplifier without arithmetic splitting?

On 03/10/2019 20:30, Peter Lammich wrote:
> 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.

So how about commenting it out for the test? See


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