| changeset 61539 | a29295dac1ca |
| parent 61486 | 3590367b0ce9 |
| child 61540 | f92bf6674699 |
--- a/src/HOL/Hahn_Banach/Linearform.thy Mon Nov 02 10:38:42 2015 +0100 +++ b/src/HOL/Hahn_Banach/Linearform.thy Mon Nov 02 11:10:28 2015 +0100 @@ -44,7 +44,7 @@ finally show ?thesis by simp qed -text \<open>Every linear form yields @{text 0} for the @{text 0} vector.\<close> +text \<open>Every linear form yields \<open>0\<close> for the \<open>0\<close> vector.\<close> lemma (in linearform) zero [iff]: assumes "vectorspace V"