src/HOL/Analysis/Norm_Arith.thy

--- a/src/HOL/Analysis/Norm_Arith.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Norm_Arith.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Author:     Amine Chaieb, University of Cambridge
 *)
 
-section \<open>General linear decision procedure for normed spaces\<close>
+section \<open>Linear Decision Procedure for Normed Spaces\<close>
 
 theory Norm_Arith
 imports "HOL-Library.Sum_of_Squares"