merged
authorwenzelm
Wed, 05 Nov 2014 22:39:49 +0100
changeset 58910 edcd9339bda1
parent 58898 1ebf0a1f12a4 (diff)
parent 58909 f323497583d1 (current diff)
child 58911 2cf595ee508b
child 58918 8d36bc5eaed3
merged
--- 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