# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530569194 -3600
# Node ID 6dff90eba4931f85856ff71fe8e7957a348cd63d
# Parent  1f86a092655bd5a48acee0d77e538a3f0a4335dc
latex fixes

diff -r 1f86a092655b -r 6dff90eba493 src/HOL/Algebra/Polynomials.thy
--- a/src/HOL/Algebra/Polynomials.thy	Mon Jul 02 22:40:25 2018 +0100
+++ b/src/HOL/Algebra/Polynomials.thy	Mon Jul 02 23:06:34 2018 +0100
@@ -377,7 +377,7 @@
 end
 
 
-subsection \<open>Poly_Add\<close>
+subsection \<open>Polynomial addition\<close>
 
 context ring
 begin
@@ -727,7 +727,7 @@
 end
 
 
-subsection \<open>Poly_Mult\<close>
+subsection \<open>Polynomial multiplication\<close>
 
 context ring
 begin
diff -r 1f86a092655b -r 6dff90eba493 src/HOL/Algebra/Ring_Divisibility.thy
--- a/src/HOL/Algebra/Ring_Divisibility.thy	Mon Jul 02 22:40:25 2018 +0100
+++ b/src/HOL/Algebra/Ring_Divisibility.thy	Mon Jul 02 23:06:34 2018 +0100
@@ -364,7 +364,7 @@
 qed
 
 
-text \<open>Helper definition for the lemma: trivial_ideal_seq_imp_noetherian\<close>
+text \<open>Helper definition for the proofs below\<close>
 fun S_builder :: "_ \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set" where
   "S_builder R J 0 = {}" |
   "S_builder R J (Suc n) =