changeset 58877 | 262572d90bc6 |
parent 53717 | 6eb85a1cb406 |
child 60420 | 884f54e01427 |
--- a/src/HOL/Multivariate_Analysis/Norm_Arith.thy Sun Nov 02 17:06:05 2014 +0100 +++ b/src/HOL/Multivariate_Analysis/Norm_Arith.thy Sun Nov 02 17:09:04 2014 +0100 @@ -2,7 +2,7 @@ Author: Amine Chaieb, University of Cambridge *) -header {* General linear decision procedure for normed spaces *} +section {* General linear decision procedure for normed spaces *} theory Norm_Arith imports "~~/src/HOL/Library/Sum_of_Squares"