equal
deleted
inserted
replaced
12 text {* |
12 text {* |
13 A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space |
13 A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space |
14 into the reals that has the following properties: it is positive |
14 into the reals that has the following properties: it is positive |
15 definite, absolute homogenous and subadditive. |
15 definite, absolute homogenous and subadditive. |
16 *} |
16 *} |
17 |
|
18 no_syntax norm :: "'a::norm \<Rightarrow> real" ("\<parallel>_\<parallel>") (* FIXME clash with Real/RealVector.thy *) |
|
19 |
17 |
20 locale norm_syntax = |
18 locale norm_syntax = |
21 fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>") |
19 fixes norm :: "'a \<Rightarrow> real" ("\<parallel>_\<parallel>") |
22 |
20 |
23 locale seminorm = var V + norm_syntax + |
21 locale seminorm = var V + norm_syntax + |