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