--- a/src/HOL/Algebra/Divisibility.thy Sun Mar 10 22:38:00 2019 +0100
+++ b/src/HOL/Algebra/Divisibility.thy Sun Mar 10 23:23:03 2019 +0100
@@ -755,8 +755,7 @@
using assms
by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l)
-(*by Paulo Emílio de Vilhena*)
-lemma (in comm_monoid_cancel) prime_irreducible:
+lemma (in comm_monoid_cancel) prime_irreducible: \<^marker>\<open>contributor \<open>Paulo Emílio de Vilhena\<close>\<close>
assumes "prime G p"
shows "irreducible G p"
proof (rule irreducibleI)