src/HOL/Library/Convex_Euclidean_Space.thy
Tue, 27 Oct 2009 12:59:57 +0000 paulson New theory SupInf of the supremum and infimum operators for sets of reals.
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Mon, 31 Aug 2009 14:09:42 +0200 nipkow tuned the simp rules for Int involving insert and intervals.
Sat, 13 Jun 2009 17:31:56 -0700 huffman generalize many constants and lemmas from Convex_Euclidean_Space
Sat, 13 Jun 2009 11:56:41 -0700 huffman replace uses of (bi)linear with bounded_(bi)linear
Fri, 12 Jun 2009 22:20:36 -0700 huffman replace all occurrences of dot at type real^'n with inner
Fri, 12 Jun 2009 12:00:30 -0700 huffman remove simp add: norm_scaleR
Fri, 12 Jun 2009 11:23:37 -0700 huffman replace all occurrences of 'op *s' at type real^'n with scaleR
Thu, 11 Jun 2009 20:04:55 -0700 huffman move lemma compact_Times; generalize more lemmas
Thu, 11 Jun 2009 11:51:12 -0700 huffman theorem attribute [tendsto_intros]
Wed, 10 Jun 2009 15:32:02 -0700 huffman rewrite proof of compact_convex_combinations to avoid pastecart and vec1
Tue, 09 Jun 2009 16:13:18 -0700 huffman remove uses of vec1 in continuity lemmas
Tue, 09 Jun 2009 11:12:08 -0700 huffman merged
Mon, 08 Jun 2009 17:15:22 -0700 huffman generalize constant 'bounded' to class metric_space
Tue, 09 Jun 2009 16:38:33 +0200 himmelma removed duplicate lemmas
Thu, 04 Jun 2009 14:32:00 -0700 huffman generalize norm method to work over class real_normed_vector
Wed, 03 Jun 2009 10:02:59 -0700 huffman generalize some constants and lemmas to class topological_space
Tue, 02 Jun 2009 23:56:12 -0700 huffman merged
Tue, 02 Jun 2009 22:09:50 -0700 huffman generalize more constants
Tue, 02 Jun 2009 10:04:03 +0200 berghofe merged
Tue, 02 Jun 2009 10:02:08 +0200 berghofe Enclosed parts of subsection in @{text ...} to make LaTeX happy.
Fri, 29 May 2009 22:42:13 -0700 huffman generalize at function to class perfect_space
Fri, 29 May 2009 18:23:07 -0700 huffman generalize topological notions to class metric_space; add class perfect_space
Thu, 28 May 2009 17:00:02 -0700 huffman move dist operation to new metric_space class
Thu, 28 May 2009 13:43:45 -0700 huffman merged
Thu, 28 May 2009 13:41:41 -0700 huffman generalize dist function to class real_normed_vector
Thu, 28 May 2009 16:19:34 +0200 himmelma Corrected definition of is_interval
Thu, 28 May 2009 15:42:44 +0200 himmelma Corrected error in Convex_Euclidean_Space
Thu, 28 May 2009 13:56:50 +0200 himmelma Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
Thu, 28 May 2009 09:46:45 +0200 himmelma Added Convex_Euclidean_Space.thy
less more (0) tip