src/HOL/Analysis/Inner_Product.thy
Tue, 22 Aug 2017 21:36:48 +0200 Manuel Eberl Lemmas about analysis and permutations
Wed, 19 Apr 2017 16:26:09 +0200 wenzelm tuned imports;
Tue, 28 Feb 2017 13:51:47 +0000 paulson Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
Mon, 17 Oct 2016 11:46:22 +0200 nipkow setsum -> sum
Fri, 30 Sep 2016 15:35:37 +0200 hoelzl HOL-Analysis: move Product_Vector and Inner_Product from Library
less more (0) tip