src/HOL/Number_Theory/Primes.thy
changeset 64911 f0e07600de47
parent 64773 223b2ebdda79
child 65025 8c32ce2a01c6
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Jan 17 11:26:21 2017 +0100
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Jan 17 13:59:10 2017 +0100
     1.3 @@ -310,7 +310,7 @@
     1.4    "prime (numeral m :: nat) \<longleftrightarrow>
     1.5      (1::nat) < numeral m \<and>
     1.6      (\<forall>n::nat\<in>set [2..<numeral m]. \<not> n dvd numeral m)"
     1.7 -  by (fact prime_nat_simp) -- \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
     1.8 +  by (fact prime_nat_simp) \<comment> \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
     1.9  
    1.10  
    1.11  text\<open>A bit of regression testing:\<close>