# HG changeset patch
# User wenzelm
# Date 1415223589 -3600
# Node ID edcd9339bda1f8d80a168f183532881b84ff02c9
# Parent  1ebf0a1f12a4816a22bdc73c1918f49afbb56fa3# Parent  f323497583d108b27f6764446e5924cf359afe9b
merged

diff -r f323497583d1 -r edcd9339bda1 src/HOL/Number_Theory/Primes.thy
--- 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