src/HOL/Analysis/Product_Vector.thy
6 months ago immler 2018-12-27 moved dependency
8 months ago haftmann 2018-11-08 removed relics of ASCII syntax for indexed big operators
9 months ago nipkow 2018-09-24 Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
12 months ago nipkow 2018-07-12 more economic tagging
12 months ago paulson 2018-07-10 de-applying, etc.
12 months ago immler 2018-07-10 make theorem, corollary, and proposition %important for HOL-Analysis manual
14 months ago immler 2018-05-02 added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
15 months ago immler 2018-04-06 a first shot at tagging for HOL-Analysis manual
16 months ago immler 2018-02-22 moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
23 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-09-30 hoelzl 2016-09-30 Library: fix name Product_plus to Product_Plus
2016-09-30 hoelzl 2016-09-30 HOL-Analysis: move Product_Vector and Inner_Product from Library