src/HOL/Real/HahnBanach/Linearform.thy
 changeset 11701 3d51fbf81c17 parent 10687 c186279eecea child 12018 ec054019c910
```     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 05 21:50:37 2001 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 05 21:52:39 2001 +0200
1.3 @@ -37,8 +37,8 @@
1.4    \<Longrightarrow> f (- x) = - f x"
1.5  proof -
1.6    assume "is_linearform V f"  "is_vectorspace V"  "x \<in> V"
1.7 -  have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1)
1.8 -  also have "... = (- #1) * (f x)" by (rule linearform_mult)
1.9 +  have "f (- x) = f ((- Numeral1) \<cdot> x)" by (simp! add: negate_eq1)
1.10 +  also have "... = (- Numeral1) * (f x)" by (rule linearform_mult)
1.11    also have "... = - (f x)" by (simp!)
1.12    finally show ?thesis .
1.13  qed
1.14 @@ -58,14 +58,14 @@
1.15  text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
1.16
1.17  lemma linearform_zero [intro?, simp]:
1.18 -  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> f 0 = #0"
1.19 +  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> f 0 = Numeral0"
1.20  proof -
1.21    assume "is_vectorspace V"  "is_linearform V f"
1.22    have "f 0 = f (0 - 0)" by (simp!)
1.23    also have "... = f 0 - f 0"
1.24      by (rule linearform_diff) (simp!)+
1.25 -  also have "... = #0" by simp
1.26 -  finally show "f 0 = #0" .
1.27 +  also have "... = Numeral0" by simp
1.28 +  finally show "f 0 = Numeral0" .
1.29  qed
1.30
1.31  end
```