reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
authorhaftmann
Sun Nov 09 10:03:18 2014 +0100 (2014-11-09)
changeset 5895418750e86d5b8
parent 58953 2e19b392d9e3
child 58955 1694bad18568
reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
src/HOL/Number_Theory/Primes.thy
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Sun Nov 09 10:03:17 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Sun Nov 09 10:03:18 2014 +0100
     1.3 @@ -154,7 +154,7 @@
     1.4  
     1.5  text{* A bit of regression testing: *}
     1.6  
     1.7 -lemma "prime(7::nat)" by simp
     1.8 +lemma "prime(97::nat)" by simp
     1.9  lemma "prime(997::nat)" by eval
    1.10  
    1.11