changeset 54230 | b1d955791529 |
parent 46867 | 0883804b67bb |
child 55018 | 2a526bd279ed |
--- a/src/HOL/Hahn_Banach/Vector_Space.thy Thu Oct 31 16:54:22 2013 +0100 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Fri Nov 01 18:51:14 2013 +0100 @@ -112,7 +112,7 @@ proof - assume x: "x \<in> V" have " (a - b) \<cdot> x = (a + - b) \<cdot> x" - by (simp add: diff_minus) + by simp also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x" by (rule add_mult_distrib2) also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"