src/HOL/Library/Product_Vector.thy
Wed, 01 Jan 2014 01:05:48 +0100 haftmann fundamental treatment of undefined vs. universally partial replaces code_abort
Mon, 16 Dec 2013 17:08:22 +0100 immler pragmatic executability of instance prod::{open,dist,norm}
Thu, 26 Sep 2013 08:44:43 -0700 huffman tuned proofs
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Tue, 09 Apr 2013 15:07:35 +0200 hoelzl add continuous_on rules for products
Tue, 09 Apr 2013 14:04:47 +0200 hoelzl move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
Thu, 31 Jan 2013 17:42:12 +0100 hoelzl remove unnecessary assumption from real_normed_vector
Fri, 19 Oct 2012 15:12:52 +0200 webertj Renamed {left,right}_distrib to distrib_{right,left}.
Tue, 06 Sep 2011 07:48:59 -0700 huffman remove redundant lemma real_sum_squared_expand in favor of power2_sum
Mon, 29 Aug 2011 08:31:09 -0700 huffman Product_Vector.thy: clean up some proofs
Sun, 28 Aug 2011 09:20:12 -0700 huffman discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Tue, 16 Aug 2011 09:31:23 -0700 huffman add simp rules for isCont
Mon, 15 Aug 2011 14:29:17 -0700 huffman Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
Tue, 09 Aug 2011 12:50:22 -0700 huffman lemma bounded_linear_intro
Tue, 09 Aug 2011 10:42:07 -0700 huffman avoid duplicate rewrite warnings
Mon, 08 Aug 2011 10:32:55 -0700 huffman rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Tue, 04 May 2010 10:42:47 -0700 huffman make (f -- a --> x) an abbreviation for (f ---> x) (at a)
Tue, 04 May 2010 10:06:05 -0700 huffman make (X ----> L) an abbreviation for (X ---> L) sequentially
Sat, 24 Apr 2010 09:37:24 -0700 huffman convert proofs to Isar-style
Sun, 29 Nov 2009 11:31:39 -0800 huffman add lemmas open_image_fst, open_image_snd
Fri, 12 Jun 2009 16:23:07 -0700 huffman declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
Fri, 12 Jun 2009 12:00:30 -0700 huffman remove simp add: norm_scaleR
Thu, 11 Jun 2009 16:26:06 -0700 huffman add lemmas about closed sets
Thu, 11 Jun 2009 11:51:12 -0700 huffman theorem attribute [tendsto_intros]
Thu, 11 Jun 2009 09:03:24 -0700 huffman cleaned up some proofs
Thu, 11 Jun 2009 08:26:08 -0700 huffman new lemmas
Sun, 07 Jun 2009 17:59:54 -0700 huffman replace 'topo' with 'open'; add extra type constraint for 'open'
Sun, 07 Jun 2009 15:18:52 -0700 huffman generalize tendsto lemmas for products
Wed, 03 Jun 2009 09:58:11 -0700 huffman replace class open with class topo
Wed, 03 Jun 2009 08:43:29 -0700 huffman instance * :: topological_space
Tue, 02 Jun 2009 23:35:52 -0700 huffman instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
Mon, 01 Jun 2009 16:59:56 -0700 huffman limits of Pair using filters
Fri, 29 May 2009 09:58:14 -0700 huffman instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
Thu, 28 May 2009 17:09:51 -0700 huffman define dist for products
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Fri, 20 Feb 2009 08:02:11 -0800 huffman add theory of products as real vector spaces to Library
less more (0) tip