src/HOL/Real/HahnBanach/Linearform.thy
changeset 7656 2f18c0ffc348
parent 7566 c5a3f980a7af
child 7808 fd019ac3485f
     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Wed Sep 29 15:35:09 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Wed Sep 29 16:41:52 1999 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4    finally; show "f (x [-] y) = f x - f y"; by (simp!);
     1.5  qed;
     1.6  
     1.7 -lemma linearform_zero [intro!!]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
     1.8 +lemma linearform_zero [intro!!, simp]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
     1.9  proof -; 
    1.10    assume "is_vectorspace V" "is_linearform V f";
    1.11    have "f <0> = f (<0> [-] <0>)"; by (simp!);