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