diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Computational_Algebra/Primes.thy --- a/src/HOL/Computational_Algebra/Primes.thy Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Computational_Algebra/Primes.thy Sun Nov 26 21:08:32 2017 +0100 @@ -271,7 +271,7 @@ subsubsection \Make prime naively executable\ lemma prime_nat_iff': - "prime (p :: nat) \ p > 1 \ (\n \ {2.. p > 1 \ (\n \ {2.. n dvd p)" proof safe assume "p > 1" and *: "\n\{2..n dvd p" show "prime p" unfolding prime_nat_iff @@ -286,7 +286,7 @@ qed (auto simp: prime_nat_iff) lemma prime_int_iff': - "prime (p :: int) \ p > 1 \ (\n \ {2.. p > 1 \ (\n \ {2.. n dvd p)" (is "?lhs = ?rhs") proof assume "?lhs" thus "?rhs" @@ -352,9 +352,9 @@ lemma primes_infinite: "\ (finite {(p::nat). prime p})" proof assume "finite {(p::nat). prime p}" - with Max_ge have "(EX b. (ALL x : {(p::nat). prime p}. x <= b))" + with Max_ge have "(\b. (\x \ {(p::nat). prime p}. x \ b))" by auto - then obtain b where "ALL (x::nat). prime x \ x <= b" + then obtain b where "\(x::nat). prime x \ x \ b" by auto with bigger_prime [of b] show False by auto