Sat, 16 Jul 2016 12:11:02 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Wed, 13 Jul 2016 20:47:56 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
Mon, 18 Apr 2016 14:30:32 +0100 |
paulson |
new theorems about convex hulls, etc.; also, renamed some theorems
|
file |
diff |
annotate
|
Thu, 25 Feb 2016 20:35:05 +0100 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
Wed, 10 Feb 2016 18:43:19 +0100 |
hoelzl |
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
|
file |
diff |
annotate
|
Tue, 17 Nov 2015 12:32:08 +0000 |
paulson |
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
|
file |
diff |
annotate
|
Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
Mon, 02 Nov 2015 11:56:28 +0100 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
Tue, 27 Oct 2015 15:17:02 +0000 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
Mon, 26 Oct 2015 23:41:27 +0000 |
paulson |
new lemmas about topology, etc., for Cauchy integral formula
|
file |
diff |
annotate
|
Tue, 13 Oct 2015 12:42:08 +0100 |
paulson |
new material on path_component_sets, inside, outside, etc. And more default simprules
|
file |
diff |
annotate
|
Mon, 31 Aug 2015 21:28:08 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
Sat, 13 Jun 2015 13:09:05 +0200 |
wenzelm |
renamed "prems" to "that";
|
file |
diff |
annotate
|
Wed, 10 Jun 2015 22:28:56 +0200 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
Tue, 26 May 2015 21:58:04 +0100 |
paulson |
New material about paths, and some lemmas
|
file |
diff |
annotate
|
Tue, 05 May 2015 18:45:10 +0200 |
immler |
generalized differentiable_bound; some further variations of differentiable_bound
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 15:00:03 +0100 |
paulson |
New material and binomial fix
|
file |
diff |
annotate
|
Thu, 19 Feb 2015 11:53:36 +0100 |
haftmann |
establish unique preferred fact names
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
Tue, 29 Apr 2014 22:50:55 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Mon, 14 Apr 2014 13:08:17 +0200 |
hoelzl |
added divide_nonneg_nonneg and co; made it a simp rule
|
file |
diff |
annotate
|
Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
Thu, 03 Apr 2014 23:51:52 +0100 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
file |
diff |
annotate
|
Tue, 04 Mar 2014 14:00:59 -0800 |
huffman |
tuned proof script
|
file |
diff |
annotate
|
Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
Fri, 13 Sep 2013 14:57:20 -0700 |
huffman |
tuned proofs about 'convex'
|
file |
diff |
annotate
|
Fri, 13 Sep 2013 11:16:13 -0700 |
huffman |
generalized and simplified proofs of several theorems about convex sets
|
file |
diff |
annotate
|
Thu, 12 Sep 2013 09:33:36 -0700 |
huffman |
new lemmas
|
file |
diff |
annotate
|
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
|
file |
diff |
annotate
|
Thu, 27 Sep 2012 14:52:50 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 18:02:16 -0700 |
huffman |
avoid warnings about duplicate rules
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 11:50:16 +0200 |
hoelzl |
lemma about differences of convex functions
|
file |
diff |
annotate
|
Mon, 23 Aug 2010 11:17:13 +0200 |
haftmann |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file |
diff |
annotate
|
Sun, 09 May 2010 22:51:11 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
Tue, 04 May 2010 18:05:22 +0200 |
hoelzl |
Add Convex to Library build
|
file |
diff |
annotate
|
Mon, 03 May 2010 14:35:10 +0200 |
hoelzl |
Moved Convex theory to library.
|
file |
diff |
annotate
|