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