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