src/HOL/Real/HahnBanach/Linearform.thy
changeset 9013 9dd0274f76af
parent 8703 816d8f6513be
child 9035 371f023d3dbd
     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Wed May 31 18:06:02 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Jun 01 11:22:27 2000 +0200
     1.3 @@ -35,8 +35,8 @@
     1.4    ==> f (- x) = - f x";
     1.5  proof -; 
     1.6    assume "is_linearform V f" "is_vectorspace V" "x:V"; 
     1.7 -  have "f (- x) = f ((- 1r) (*) x)"; by (simp! add: negate_eq1);
     1.8 -  also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
     1.9 +  have "f (- x) = f ((- (#1::real)) (*) x)"; by (simp! add: negate_eq1);
    1.10 +  also; have "... = (- #1) * (f x)"; by (rule linearform_mult);
    1.11    also; have "... = - (f x)"; by (simp!);
    1.12    finally; show ?thesis; .;
    1.13  qed;
    1.14 @@ -56,14 +56,14 @@
    1.15  text{* Every linear form yields $0$ for the $\zero$ vector.*};
    1.16  
    1.17  lemma linearform_zero [intro??, simp]: 
    1.18 -  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = 0r"; 
    1.19 +  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = (#0::real)"; 
    1.20  proof -; 
    1.21    assume "is_vectorspace V" "is_linearform V f";
    1.22    have "f 00 = f (00 - 00)"; by (simp!);
    1.23    also; have "... = f 00 - f 00"; 
    1.24      by (rule linearform_diff) (simp!)+;
    1.25 -  also; have "... = 0r"; by simp;
    1.26 -  finally; show "f 00 = 0r"; .;
    1.27 +  also; have "... = (#0::real)"; by simp;
    1.28 +  finally; show "f 00 = (#0::real)"; .;
    1.29  qed; 
    1.30  
    1.31  end;
    1.32 \ No newline at end of file