src/HOL/Analysis/Product_Vector.thy
Fri, 12 Apr 2019 22:24:07 +0200 wenzelm tuned spacing;
Fri, 12 Apr 2019 22:09:25 +0200 wenzelm modernized tags: default scope excludes proof;
Sat, 29 Dec 2018 17:46:48 +0100 immler tuned analysis manual
Thu, 27 Dec 2018 21:00:54 +0100 immler moved dependency
Thu, 08 Nov 2018 09:11:52 +0100 haftmann removed relics of ASCII syntax for indexed big operators
Mon, 24 Sep 2018 14:30:09 +0200 nipkow Prefix form of infix with * on either side no longer needs special treatment
Thu, 12 Jul 2018 11:23:46 +0200 nipkow more economic tagging
Tue, 10 Jul 2018 23:18:08 +0100 paulson de-applying, etc.
Tue, 10 Jul 2018 09:38:35 +0200 immler make theorem, corollary, and proposition %important for HOL-Analysis manual
Wed, 02 May 2018 13:49:38 +0200 immler added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
Fri, 06 Apr 2018 17:34:50 +0200 immler a first shot at tagging for HOL-Analysis manual
Thu, 22 Feb 2018 15:17:25 +0100 immler moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
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