src/HOL/Multivariate_Analysis/L2_Norm.thy

--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Jun 10 19:05:19 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Jun 10 19:10:20 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Brian Huffman, Portland State University
 *)
 
-section {* Square root of sum of squares *}
+section \<open>Square root of sum of squares\<close>
 
 theory L2_Norm
 imports NthRoot