--- 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
--- 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) =