Fixed sectioning in HOL/Library/Polynomial
authoreberlm
Tue Jan 05 20:23:49 2016 +0100 (2016-01-05)
changeset 620670fd850943901
parent 62066 4db2d39aa76c
child 62071 4e6e850e97c2
Fixed sectioning in HOL/Library/Polynomial
src/HOL/Library/Polynomial.thy
     1.1 --- a/src/HOL/Library/Polynomial.thy	Tue Jan 05 17:54:21 2016 +0100
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Tue Jan 05 20:23:49 2016 +0100
     1.3 @@ -2190,7 +2190,7 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -section{*lead coefficient*}
     1.8 +subsection {* Leading coefficient *}
     1.9  
    1.10  definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
    1.11    "lead_coeff p= coeff p (degree p)"