--- a/src/HOL/Number_Theory/Primes.thy Wed Nov 05 22:37:14 2014 +0100+++ b/src/HOL/Number_Theory/Primes.thy Wed Nov 05 22:39:49 2014 +0100@@ -154,7 +154,7 @@ text{* A bit of regression testing: *}-lemma "prime(97::nat)" by simp+lemma "prime(7::nat)" by simp lemma "prime(997::nat)" by eval