# HG changeset patch
# User eberlm
# Date 1452021829 -3600
# Node ID 0fd850943901a5e20858cdfbdab01d3fbc125fcf
# Parent  4db2d39aa76c0f11ac41521b45f8cdc9e4e44a6b
Fixed sectioning in HOL/Library/Polynomial

diff -r 4db2d39aa76c -r 0fd850943901 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Tue Jan 05 17:54:21 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Tue Jan 05 20:23:49 2016 +0100
@@ -2190,7 +2190,7 @@
 qed
 
 
-section{*lead coefficient*}
+subsection {* Leading coefficient *}
 
 definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
   "lead_coeff p= coeff p (degree p)"