src/HOL/Multivariate_Analysis/Linear_Algebra.thy
Fri, 28 Sep 2012 23:02:49 +0200 wenzelm tuned proofs;
Sat, 22 Sep 2012 17:55:56 +0200 wenzelm misc tuning;
Fri, 21 Sep 2012 22:45:14 +0200 wenzelm tuned proofs;
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Tue, 06 Sep 2011 08:00:28 -0700 huffman remove duplicate copy of lemma sqrt_add_le_add_sqrt
Tue, 06 Sep 2011 07:48:59 -0700 huffman remove redundant lemma real_sum_squared_expand in favor of power2_sum
Fri, 02 Sep 2011 13:57:12 -0700 huffman remove more duplicate lemmas
Thu, 01 Sep 2011 07:31:33 -0700 huffman add lemma tendsto_infnorm
Wed, 31 Aug 2011 13:51:22 -0700 huffman remove redundant lemma card_enum
Thu, 25 Aug 2011 16:42:13 -0700 huffman arrange everything related to ordered_euclidean_space class together
Thu, 25 Aug 2011 16:06:50 -0700 huffman generalize and shorten proof of basis_orthogonal
Thu, 25 Aug 2011 15:35:54 -0700 huffman remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
Thu, 25 Aug 2011 11:57:42 -0700 huffman simplify many proofs about subspace and span;
Wed, 24 Aug 2011 15:32:40 -0700 huffman minimize imports
Wed, 24 Aug 2011 15:06:13 -0700 huffman move everything related to 'norm' method into new theory file Norm_Arith.thy
Wed, 24 Aug 2011 12:39:42 -0700 huffman remove unused lemmas dimensionI, dimension_eq
Wed, 24 Aug 2011 11:56:57 -0700 huffman move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
Tue, 23 Aug 2011 16:17:22 -0700 huffman move connected_real_lemma to the one place it is used
Tue, 23 Aug 2011 14:11:02 -0700 huffman declare euclidean_simps [simp] at the point they are proved;
Mon, 22 Aug 2011 17:22:49 -0700 huffman avoid warnings
Mon, 22 Aug 2011 10:19:39 -0700 huffman remove duplicate lemma
Sun, 21 Aug 2011 09:46:20 -0700 huffman section -> subsection
Thu, 18 Aug 2011 18:08:43 -0700 huffman import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
Thu, 18 Aug 2011 17:32:02 -0700 huffman declare euclidean_component_zero[simp] at the point it is proved
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Fri, 12 Aug 2011 20:55:22 -0700 huffman remove redundant lemma setsum_norm in favor of norm_setsum;
Fri, 12 Aug 2011 09:17:24 -0700 huffman make Multivariate_Analysis work with separate set type
Thu, 11 Aug 2011 13:05:56 -0700 huffman modify euclidean_space class to include basis set
Wed, 10 Aug 2011 18:02:16 -0700 huffman avoid warnings about duplicate rules
Wed, 10 Aug 2011 09:23:42 -0700 huffman split Linear_Algebra.thy from Euclidean_Space.thy
less more (0) tip