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
```