src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Mon, 14 Nov 2011 09:49:05 +0100 huffman avoid numeral-representation-specific rules in metis proof
Thu, 22 Sep 2011 14:12:16 -0700 huffman discontinued legacy theorem names from RealDef.thy
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Wed, 07 Sep 2011 09:02:58 -0700 huffman avoid using legacy theorem names
Thu, 01 Sep 2011 09:02:14 -0700 huffman modernize lemmas about 'continuous' and 'continuous_on';
Wed, 31 Aug 2011 13:51:22 -0700 huffman remove redundant lemma card_enum
Thu, 25 Aug 2011 19:41:38 -0700 huffman replace some continuous_on lemmas with more general versions
Thu, 25 Aug 2011 14:25:19 -0700 huffman generalize lemma finite_imp_compact_convex_hull and related lemmas
Thu, 25 Aug 2011 13:48:11 -0700 huffman generalize some lemmas
Thu, 25 Aug 2011 12:52:10 -0700 huffman generalize lemma convex_cone_hull
Thu, 25 Aug 2011 12:43:55 -0700 huffman rename subset_{interior,closure} to {interior,closure}_mono;
Thu, 25 Aug 2011 09:17:02 -0700 huffman simplify definition of 'interior';
Wed, 24 Aug 2011 09:08:00 -0700 huffman change some subsection headings to subsubsection
Tue, 23 Aug 2011 16:47:48 -0700 huffman remove unnecessary lemma card_ge1
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;
Sun, 21 Aug 2011 12:22:31 -0700 huffman add lemmas interior_Times and closure_Times
Sun, 21 Aug 2011 11:03:15 -0700 huffman remove unnecessary euclidean_space class constraints
Sat, 20 Aug 2011 15:54:26 -0700 huffman remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
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 09:17:24 -0700 huffman make Multivariate_Analysis work with separate set type
Wed, 10 Aug 2011 18:02:16 -0700 huffman avoid warnings about duplicate rules
Wed, 10 Aug 2011 08:42:26 -0700 huffman full import paths
Tue, 09 Aug 2011 10:30:00 -0700 huffman mark some redundant theorems as legacy
Sat, 30 Jul 2011 08:24:46 +0200 haftmann tuned proofs
Mon, 25 Jul 2011 23:26:55 +0200 haftmann adjusted to tailored version of ball_simps
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Fri, 03 Dec 2010 00:36:01 +0100 hoelzl adapt proofs to changed set_plus_image (cf. ee8d0548c148);
Thu, 02 Dec 2010 16:45:28 +0100 hoelzl Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
Fri, 26 Nov 2010 21:09:36 +0100 wenzelm keep private things private, without comments;
Fri, 05 Nov 2010 14:17:18 +0100 hoelzl Extend convex analysis by Bogdan Grechuk
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
Mon, 23 Aug 2010 11:17:13 +0200 haftmann dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
Mon, 05 Jul 2010 09:14:51 -0700 huffman generalize type of is_interval to class euclidean_space
Thu, 01 Jul 2010 09:24:04 -0700 huffman generalize more lemmas from ordered_euclidean_space to euclidean_space
Wed, 30 Jun 2010 11:51:35 -0700 huffman minimize dependencies on Numeral_Type
Mon, 21 Jun 2010 19:33:51 +0200 hoelzl Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
Tue, 11 May 2010 19:21:05 +0200 hoelzl Removed usage of normalizating locales.
Sun, 09 May 2010 22:51:11 -0700 huffman avoid using real-specific versions of generic lemmas
Fri, 07 May 2010 09:59:24 +0200 haftmann prefix normalizing replaces class_semiring
Thu, 06 May 2010 23:11:57 +0200 haftmann former free-floating field_comp_conv now in structure Normalizer
Mon, 03 May 2010 10:28:19 -0700 huffman merged
Sat, 01 May 2010 07:35:22 -0700 huffman move setsum lemmas to Product_plus.thy
Mon, 03 May 2010 14:35:10 +0200 hoelzl Moved Convex theory to library.
Thu, 29 Apr 2010 07:22:01 -0700 huffman remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
Wed, 28 Apr 2010 22:02:55 -0700 huffman remove redundant lemma norm_0
Wed, 28 Apr 2010 16:11:07 -0700 huffman move path-related stuff into new theory file
Tue, 27 Apr 2010 11:03:04 -0700 huffman generalize types of path operations
Mon, 26 Apr 2010 12:19:57 -0700 huffman move definitions and theorems for type real^1 to separate theory file
Mon, 26 Apr 2010 09:45:22 -0700 huffman merged
Mon, 26 Apr 2010 09:21:25 -0700 huffman fix lots of looping simp calls and other warnings
Mon, 26 Apr 2010 11:34:19 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps
Sun, 25 Apr 2010 10:23:03 -0700 huffman generalize more constants and lemmas
Sun, 25 Apr 2010 09:01:03 -0700 huffman simplify types of path operations (use real instead of real^1)
Sun, 25 Apr 2010 07:41:57 -0700 huffman add lemmas convex_real_interval and convex_box
Sat, 24 Apr 2010 21:29:22 -0700 huffman generalize more constants and lemmas
Sat, 24 Apr 2010 19:32:20 -0700 huffman generalize constant closest_point
less more (0) -60 tip