# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1555239594 -3600
# Node ID 13b10ca7115021fc1a548364b234a303ea6acb75
# Parent  4c3bb14f5c2b28c1ea8cd6bdfc2fa658128d5009
markup fixes

diff -r 4c3bb14f5c2b -r 13b10ca71150 src/HOL/Algebra/Indexed_Polynomials.thy
--- 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>
 
diff -r 4c3bb14f5c2b -r 13b10ca71150 src/HOL/Algebra/Polynomial_Divisibility.thy
--- 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])"