--- a/src/HOL/Deriv.thy Sun Nov 02 18:21:14 2014 +0100 +++ b/src/HOL/Deriv.thy Sun Nov 02 18:21:45 2014 +0100 @@ -6,7 +6,7 @@ GMVT by Benjamin Porter, 2005 *) -header{* Differentiation *} +section{* Differentiation *} theory Deriv imports Limits