--- a/src/HOL/Algebra/Indexed_Polynomials.thy Sat Apr 13 19:27:37 2019 +0100
+++ b/src/HOL/Algebra/Indexed_Polynomials.thy Sun Apr 14 11:59:54 2019 +0100
@@ -336,7 +336,7 @@
qed
-subsection \<open>Link with Weak_Morphisms\<close>
+subsection \<open>Link with Weak Morphisms\<close>
text \<open>We study some elements of the contradiction needed in the algebraic closure existence proof. \<close>
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy Sat Apr 13 19:27:37 2019 +0100
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy Sun Apr 14 11:59:54 2019 +0100
@@ -897,7 +897,7 @@
qed
-subsection \<open>Link between pmod and rupture_surj\<close>
+subsection \<open>Link between @{term \<open>(pmod)\<close>} and @{term rupture_surj}\<close>
lemma (in domain) rupture_surj_composed_with_pmod:
assumes "subfield K R" and "p \<in> carrier (K[X])" and "q \<in> carrier (K[X])"