[isabelle] [Isabelle2016-1-RC4] Simplification of numerals very slow when Primes is imported
while updating some of my theories to Isabelle2016-1, I noticed that simplification of some goals
involving numerals is extremely slow when the "Primes" theory is imported. In the attachment, you
can find a small theory containing two applications of "simp". When the Primes theory is loaded,
the first application takes about a minute to complete, whereas the second one returns almost
immediately. When importing Main instead of Primes, both invocations of simp are equally fast.
I did not observe this behaviour with Isabelle2016. Does anyone have an idea what is going wrong?
Perhaps the simpset got messed up during the recent update of the number theory library?
(* very slow when Primes theory is loaded *)
lemma "((foo::int) + bar * xxx mod 2 ^ 8) mod 2 ^ 8 = baz"
(* this one is faster *)
lemma "((foo::int) + bar * xxx) mod 2 ^ 8 = baz"
This archive was generated by a fusion of
Pipermail (Mailman edition) and