src/HOL/Analysis/Product_Vector.thy
changeset 63972 c98d1dd7eba1
parent 63971 da89140186e2
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Analysis/Product_Vector.thy	Fri Sep 30 15:35:37 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Fri Sep 30 15:35:43 2016 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  theory Product_Vector
     1.5  imports
     1.6    Inner_Product
     1.7 -  "~~/src/HOL/Library/Product_plus"
     1.8 +  "~~/src/HOL/Library/Product_Plus"
     1.9  begin
    1.10  
    1.11  subsection \<open>Product is a real vector space\<close>