src/HOL/Computational_Algebra/Primes.thy
 changeset 67091 1393c2340eec parent 67051 e7e54a0b9197 child 67117 19f627407264
```     1.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Sun Nov 26 13:19:52 2017 +0100
1.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Sun Nov 26 21:08:32 2017 +0100
1.3 @@ -271,7 +271,7 @@
1.4  subsubsection \<open>Make prime naively executable\<close>
1.5
1.6  lemma prime_nat_iff':
1.7 -  "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)"
1.8 +  "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
1.9  proof safe
1.10    assume "p > 1" and *: "\<forall>n\<in>{2..<p}. \<not>n dvd p"
1.11    show "prime p" unfolding prime_nat_iff
1.12 @@ -286,7 +286,7 @@
1.13  qed (auto simp: prime_nat_iff)
1.14
1.15  lemma prime_int_iff':
1.16 -  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)" (is "?lhs = ?rhs")
1.17 +  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?lhs = ?rhs")
1.18  proof
1.19    assume "?lhs"
1.20    thus "?rhs"
1.21 @@ -352,9 +352,9 @@
1.22  lemma primes_infinite: "\<not> (finite {(p::nat). prime p})"
1.23  proof
1.24    assume "finite {(p::nat). prime p}"
1.25 -  with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))"
1.26 +  with Max_ge have "(\<exists>b. (\<forall>x \<in> {(p::nat). prime p}. x \<le> b))"
1.27      by auto
1.28 -  then obtain b where "ALL (x::nat). prime x \<longrightarrow> x <= b"
1.29 +  then obtain b where "\<forall>(x::nat). prime x \<longrightarrow> x \<le> b"
1.30      by auto
1.31    with bigger_prime [of b] show False
1.32      by auto
```