Fri, 30 Sep 2016 15:35:43 +0200 Library: fix name Product_plus to Product_Plus
hoelzl [Fri, 30 Sep 2016 15:35:43 +0200] rev 63972
Library: fix name Product_plus to Product_Plus
Fri, 30 Sep 2016 15:35:37 +0200 HOL-Analysis: move Product_Vector and Inner_Product from Library
hoelzl [Fri, 30 Sep 2016 15:35:37 +0200] rev 63971
HOL-Analysis: move Product_Vector and Inner_Product from Library
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 tip