--- a/src/HOL/Algebra/Divisibility.thy Mon Aug 08 14:13:14 2016 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Mon Aug 08 17:47:51 2016 +0200
@@ -2250,7 +2250,7 @@
subsection \<open>Irreducible Elements are Prime\<close>
-lemma (in factorial_monoid) irreducible_is_prime:
+lemma (in factorial_monoid) irreducible_prime:
assumes pirr: "irreducible G p"
and pcarr: "p \<in> carrier G"
shows "prime G p"
@@ -2340,7 +2340,7 @@
\<comment>"A version using @{const factors}, more complicated"
-lemma (in factorial_monoid) factors_irreducible_is_prime:
+lemma (in factorial_monoid) factors_irreducible_prime:
assumes pirr: "irreducible G p"
and pcarr: "p \<in> carrier G"
shows "prime G p"
@@ -3638,7 +3638,7 @@
done
sublocale factorial_monoid \<subseteq> primeness_condition_monoid
- by standard (rule irreducible_is_prime)
+ by standard (rule irreducible_prime)
lemma (in factorial_monoid) primeness_condition: