summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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