diff -r 2c01c0bdb385 -r d3eb431db035 src/HOL/Real/HahnBanach/Linearform.thy
--- a/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 16:50:09 2008 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 19:39:37 2008 +0200
@@ -5,7 +5,9 @@
header {* Linearforms *}
-theory Linearform imports VectorSpace begin
+theory Linearform
+imports VectorSpace
+begin
text {*
A \emph{linear form} is a function on a vector space into the reals
@@ -25,9 +27,9 @@
proof -
interpret vectorspace [V] by fact
assume x: "x \ V"
- hence "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1)
- also from x have "... = (- 1) * (f x)" by (rule mult)
- also from x have "... = - (f x)" by simp
+ then have "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1)
+ also from x have "\ = (- 1) * (f x)" by (rule mult)
+ also from x have "\ = - (f x)" by simp
finally show ?thesis .
qed
@@ -37,8 +39,8 @@
proof -
interpret vectorspace [V] by fact
assume x: "x \ V" and y: "y \ V"
- hence "x - y = x + - y" by (rule diff_eq1)
- also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)
+ then have "x - y = x + - y" by (rule diff_eq1)
+ also have "f \ = f x + f (- y)" by (rule add) (simp_all add: x y)
also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
finally show ?thesis by simp
qed