src/HOL/Real_Vector_Spaces.thy
changeset 57276 49c51eeaa623
parent 57275 0ddb5b755cdc
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Jun 18 07:31:12 2014 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Jun 18 14:31:32 2014 +0200
     1.3 @@ -1862,3 +1862,4 @@
     1.4  qed
     1.5  
     1.6  end
     1.7 +