src/HOL/RealVector.thy
Sun, 28 Aug 2011 20:56:49 -0700 huffman move class perfect_space into RealVector.thy;
Thu, 18 Aug 2011 13:36:58 -0700 huffman remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
Tue, 09 Aug 2011 12:50:22 -0700 huffman lemma bounded_linear_intro
Mon, 14 Mar 2011 14:37:33 +0100 hoelzl moved t2_spaces to HOL image
Fri, 20 Aug 2010 17:46:56 +0200 haftmann more concise characterization of of_nat operation and class semiring_char_0
Mon, 19 Jul 2010 16:09:44 +0200 haftmann diff_minus subsumes diff_def
Mon, 12 Jul 2010 10:48:37 +0200 haftmann dropped superfluous [code del]s
Tue, 11 May 2010 18:06:58 -0700 huffman no more RealPow.thy (remaining lemmas moved to RealDef.thy)
Mon, 10 May 2010 12:12:58 -0700 huffman new construction of real numbers using Cauchy sequences
Mon, 26 Apr 2010 15:37:50 +0200 haftmann use new classes (linordered_)field_inverse_zero
Mon, 26 Apr 2010 11:34:17 +0200 haftmann class division_ring_inverse_zero
Thu, 18 Feb 2010 14:21:44 -0800 huffman get rid of many duplicate simp rule warnings
Fri, 12 Jun 2009 11:39:23 -0700 huffman declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]
Thu, 11 Jun 2009 15:33:13 -0700 huffman new lemmas
Thu, 11 Jun 2009 11:51:12 -0700 huffman theorem attribute [tendsto_intros]
Thu, 11 Jun 2009 10:37:02 -0700 huffman subsection for real instances; new lemmas for open sets of reals
Sun, 07 Jun 2009 20:57:24 -0700 huffman fix type of open
Sun, 07 Jun 2009 17:59:54 -0700 huffman replace 'topo' with 'open'; add extra type constraint for 'open'
Sun, 07 Jun 2009 12:00:03 -0700 huffman move definitions of open, closed to RealVector.thy
Thu, 04 Jun 2009 16:11:36 -0700 huffman add extra type constraints for dist, norm
Wed, 03 Jun 2009 10:29:11 -0700 huffman more [code del] declarations
Wed, 03 Jun 2009 09:58:11 -0700 huffman replace class open with class topo
Wed, 03 Jun 2009 07:44:56 -0700 huffman introduce class topological_space as a superclass of metric_space
Thu, 28 May 2009 17:00:02 -0700 huffman move dist operation to new metric_space class
Thu, 28 May 2009 13:41:41 -0700 huffman generalize dist function to class real_normed_vector
Tue, 28 Apr 2009 15:50:30 +0200 haftmann stripped class recpower further
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Wed, 04 Mar 2009 17:12:23 -0800 huffman declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Sun, 22 Feb 2009 12:48:49 -0800 huffman declare scaleR distrib rules [algebra_simps]; cleaned up
Sun, 22 Feb 2009 12:16:51 -0800 huffman clean up instantiations
Wed, 21 Jan 2009 23:40:23 +0100 haftmann no base sort in class import
Tue, 30 Dec 2008 11:10:01 +0100 ballarin Merged.
Mon, 29 Dec 2008 14:08:08 +0100 haftmann adapted HOL source structure to distribution layout
less more (0) tip