--- a/NEWS Tue Aug 09 11:57:24 2016 +0200
+++ b/NEWS Tue Aug 09 12:30:31 2016 +0200
@@ -197,10 +197,12 @@
clashes.
INCOMPATIBILITY.
-* Number_Theory: algebraic foundation for primes: Introduction of
-predicates "is_prime", "irreducible", a "prime_factorization"
-function, the "factorial_ring" typeclass with instance proofs for
-nat, int, poly.
+* Number_Theory: algebraic foundation for primes: Generalisation of
+predicate "prime" and introduction of predicates "prime_elem",
+"irreducible", a "prime_factorization" function, and the "factorial_ring"
+typeclass with instance proofs for nat, int, poly. Some theorems now have
+different names, most notably "prime_def" is now "prime_nat_iff".
+INCOMPATIBILITY.
* Probability: Code generation and QuickCheck for Probability Mass
Functions.
--- a/src/HOL/Number_Theory/Primes.thy Tue Aug 09 11:57:24 2016 +0200
+++ b/src/HOL/Number_Theory/Primes.thy Tue Aug 09 12:30:31 2016 +0200
@@ -243,7 +243,7 @@
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
-lemma two_prime_nat [simp]: "prime (2::nat)"
+lemma two_is_prime_nat [simp]: "prime (2::nat)"
by simp
declare prime_int_nat_transfer[of "numeral m" for m, simp]
@@ -615,4 +615,4 @@
lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/Sqrt.thy Tue Aug 09 11:57:24 2016 +0200
+++ b/src/HOL/ex/Sqrt.thy Tue Aug 09 12:30:31 2016 +0200
@@ -14,7 +14,7 @@
assumes "prime (p::nat)"
shows "sqrt p \<notin> \<rat>"
proof
- from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
+ from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_iff)
assume "sqrt p \<in> \<rat>"
then obtain m n :: nat where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
@@ -59,7 +59,7 @@
assumes "prime (p::nat)"
shows "sqrt p \<notin> \<rat>"
proof
- from \<open>prime p\<close> have p: "1 < p" by (simp add: is_prime_nat_iff)
+ from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_iff)
assume "sqrt p \<in> \<rat>"
then obtain m n :: nat where
n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
--- a/src/HOL/ex/Sqrt_Script.thy Tue Aug 09 11:57:24 2016 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy Tue Aug 09 12:30:31 2016 +0200
@@ -17,7 +17,7 @@
subsection \<open>Preliminaries\<close>
lemma prime_nonzero: "prime (p::nat) \<Longrightarrow> p \<noteq> 0"
- by (force simp add: is_prime_nat_iff)
+ by (force simp add: prime_nat_iff)
lemma prime_dvd_other_side:
"(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
@@ -32,7 +32,7 @@
apply (erule disjE)
apply (frule mult_le_mono, assumption)
apply auto
- apply (force simp add: is_prime_nat_iff)
+ apply (force simp add: prime_nat_iff)
done
lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"