| changeset 61486 | 3590367b0ce9 |
| parent 61076 | bdc1e2f0a86a |
| child 61539 | a29295dac1ca |
--- a/src/HOL/Hahn_Banach/Linearform.thy Mon Oct 19 17:19:53 2015 +0200 +++ b/src/HOL/Hahn_Banach/Linearform.thy Mon Oct 19 17:45:36 2015 +0200 @@ -9,7 +9,7 @@ begin text \<open> - A \emph{linear form} is a function on a vector space into the reals + A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is additive and multiplicative. \<close>