--- a/src/HOL/Real_Vector_Spaces.thy Mon Feb 08 17:18:13 2016 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Mon Feb 08 19:53:49 2016 +0100 @@ -2143,4 +2143,3 @@ qed end -