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

src/HOL/Real/HahnBanach/Linearform.thy

changeset 23378 | 1d138d6bb461 |

parent 16417 | 9bc16273c2d4 |

child 25762 | c03e9d04b3e4 |

1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy Wed Jun 13 19:14:51 2007 +0200 1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Thu Jun 14 00:22:45 2007 +0200 1.3 @@ -36,7 +36,7 @@ 1.4 assume x: "x \<in> V" and y: "y \<in> V" 1.5 hence "x - y = x + - y" by (rule diff_eq1) 1.6 also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y) 1.7 - also from _ y have "f (- y) = - f y" by (rule neg) 1.8 + also have "f (- y) = - f y" using `vectorspace V` y by (rule neg) 1.9 finally show ?thesis by simp 1.10 qed 1.11 1.12 @@ -47,7 +47,7 @@ 1.13 shows "f 0 = 0" 1.14 proof - 1.15 have "f 0 = f (0 - 0)" by simp 1.16 - also have "\<dots> = f 0 - f 0" by (rule diff) simp_all 1.17 + also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all 1.18 also have "\<dots> = 0" by simp 1.19 finally show ?thesis . 1.20 qed