src/HOL/Analysis/Product_Vector.thy
Fri, 30 Sep 2016 15:35:43 +0200 hoelzl Library: fix name Product_plus to Product_Plus
Fri, 30 Sep 2016 15:35:37 +0200 hoelzl HOL-Analysis: move Product_Vector and Inner_Product from Library
less more (0) tip