[isabelle-dev] HOL/Number_Theory/Primes

Lawrence Paulson lp15 at cam.ac.uk
Wed Nov 5 18:36:35 CET 2014


This theory takes quite a while to load, and I have found out why:

text{* A bit of regression testing: *}

lemma "prime(97::nat)" by simp
lemma "prime(997::nat)" by eval

The proof that 97 is prime takes 35 seconds on a very fast machine. Can we get rid of this or at least substitute a smaller number?

Larry




More information about the isabelle-dev mailing list