src/HOL/Analysis/Inner_Product.thy
2017-04-19 wenzelm 2017-04-19 tuned imports;
2017-02-28 paulson 2017-02-28 Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Product_Vector and Inner_Product from Library