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