equal
deleted
inserted
replaced
40 |
40 |
41 theory Primes |
41 theory Primes |
42 imports Euclidean_Algorithm |
42 imports Euclidean_Algorithm |
43 begin |
43 begin |
44 |
44 |
45 subsection \<open>Primes on @{typ nat} and @{typ int}\<close> |
45 subsection \<open>Primes on \<^typ>\<open>nat\<close> and \<^typ>\<open>int\<close>\<close> |
46 |
46 |
47 lemma Suc_0_not_prime_nat [simp]: "\<not> prime (Suc 0)" |
47 lemma Suc_0_not_prime_nat [simp]: "\<not> prime (Suc 0)" |
48 using not_prime_1 [where ?'a = nat] by simp |
48 using not_prime_1 [where ?'a = nat] by simp |
49 |
49 |
50 lemma prime_ge_2_nat: |
50 lemma prime_ge_2_nat: |