src/HOL/Library/Inner_Product.thy
Thu, 03 Apr 2014 17:56:08 +0200 hoelzl merged DERIV_intros, has_derivative_intros into derivative_intros
Mon, 17 Mar 2014 19:12:52 +0100 hoelzl unify syntax for has_derivative and differentiable
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Thu, 26 Sep 2013 16:33:32 -0700 huffman moved lemma
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 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
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}.
Mon, 12 Sep 2011 09:21:01 -0700 huffman move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
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
Tue, 09 Aug 2011 10:42:07 -0700 huffman avoid duplicate rewrite warnings
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Fri, 12 Jun 2009 16:23:07 -0700 huffman declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
Sun, 07 Jun 2009 17:59:54 -0700 huffman replace 'topo' with 'open'; add extra type constraint for 'open'
Thu, 04 Jun 2009 16:11:36 -0700 huffman add extra type constraints for dist, norm
Wed, 03 Jun 2009 09:58:11 -0700 huffman replace class open with class topo
Wed, 03 Jun 2009 08:43:01 -0700 huffman class real_inner derives from open_dist
Thu, 28 May 2009 17:00:02 -0700 huffman move dist operation to new metric_space class
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Mon, 23 Mar 2009 08:14:24 +0100 haftmann Main is (Complex_Main) base entry point in library theories
Sun, 22 Feb 2009 10:53:10 -0800 huffman simplify some proofs
Sat, 21 Feb 2009 16:51:42 -0800 huffman fix spelling
Thu, 19 Feb 2009 09:42:23 -0800 huffman new theory of real inner product spaces
less more (0) tip