# HG changeset patch
# User nipkow
# Date 1415212997 -3600
# Node ID 1ebf0a1f12a4816a22bdc73c1918f49afbb56fa3
# Parent  527bd5a7e9f8f2ba04b3f8354fe7229dd447e53c
reduced execution time

diff -r 527bd5a7e9f8 -r 1ebf0a1f12a4 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Tue Nov 04 18:19:38 2014 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Wed Nov 05 19:43:17 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