src/HOL/Real/HahnBanach/Linearform.thy
changeset 27612 d3eb431db035
parent 27611 2c01c0bdb385
child 29234 60f7fb56f8cd
     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Tue Jul 15 16:50:09 2008 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Tue Jul 15 19:39:37 2008 +0200
     1.3 @@ -5,7 +5,9 @@
     1.4  
     1.5  header {* Linearforms *}
     1.6  
     1.7 -theory Linearform imports VectorSpace begin
     1.8 +theory Linearform
     1.9 +imports VectorSpace
    1.10 +begin
    1.11  
    1.12  text {*
    1.13    A \emph{linear form} is a function on a vector space into the reals
    1.14 @@ -25,9 +27,9 @@
    1.15  proof -
    1.16    interpret vectorspace [V] by fact
    1.17    assume x: "x \<in> V"
    1.18 -  hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
    1.19 -  also from x have "... = (- 1) * (f x)" by (rule mult)
    1.20 -  also from x have "... = - (f x)" by simp
    1.21 +  then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
    1.22 +  also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
    1.23 +  also from x have "\<dots> = - (f x)" by simp
    1.24    finally show ?thesis .
    1.25  qed
    1.26  
    1.27 @@ -37,8 +39,8 @@
    1.28  proof -
    1.29    interpret vectorspace [V] by fact
    1.30    assume x: "x \<in> V" and y: "y \<in> V"
    1.31 -  hence "x - y = x + - y" by (rule diff_eq1)
    1.32 -  also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)
    1.33 +  then have "x - y = x + - y" by (rule diff_eq1)
    1.34 +  also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
    1.35    also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
    1.36    finally show ?thesis by simp
    1.37  qed