src/HOL/HahnBanach/Subspace.thy
changeset 30729 461ee3e49ad3
parent 29252 ea97aa6aeba2
     1.1 --- a/src/HOL/HahnBanach/Subspace.thy	Thu Mar 26 19:24:21 2009 +0100
     1.2 +++ b/src/HOL/HahnBanach/Subspace.thy	Thu Mar 26 20:08:55 2009 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4    assumes "vectorspace V"
     1.5    shows "0 \<in> U"
     1.6  proof -
     1.7 -  interpret V!: vectorspace V by fact
     1.8 +  interpret V: vectorspace V by fact
     1.9    have "U \<noteq> {}" by (rule non_empty)
    1.10    then obtain x where x: "x \<in> U" by blast
    1.11    then have "x \<in> V" .. then have "0 = x - x" by simp