| Fri, 08 Jan 2016 15:49:01 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 13:42:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 17:40:55 +0000 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 17:43:30 +0100 |
wenzelm |
prefer symbols for "Union", "Inter";
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:28:28 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 17 Dec 2015 16:43:36 +0100 |
hoelzl |
moved some theorems from the CLT proof; reordered some theorems / notation
|
file |
diff |
annotate
|
| Tue, 15 Dec 2015 14:40:36 +0000 |
paulson |
New complex analysis material
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 20:19:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 14:09:10 +0000 |
paulson |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
file |
diff |
annotate
|
| Mon, 23 Nov 2015 16:57:54 +0000 |
paulson |
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
|
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
|
| Tue, 10 Nov 2015 14:18:41 +0000 |
paulson |
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
|
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, 21 Sep 2015 21:46:14 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Thu, 03 Sep 2015 20:27:53 +0100 |
paulson |
new lemmas about vector_derivative, complex numbers, paths, etc.
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Wed, 19 Aug 2015 19:18:19 +0100 |
paulson |
New material and fixes related to the forthcoming Stone-Weierstrass development
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 16:16:13 +0100 |
paulson |
the Cauchy integral theorem and related material
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 16:52:57 +0100 |
paulson |
New material for Cauchy's integral theorem
|
file |
diff |
annotate
|
| Mon, 20 Jul 2015 23:12:50 +0100 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 10:20:33 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 19:10:20 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Thu, 28 May 2015 14:33:35 +0100 |
paulson |
Convex hulls: theorems about interior, etc. And a few simple lemmas.
|
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 |
closures of intervals
|
file |
diff |
annotate
|
| Wed, 25 Mar 2015 10:44:57 +0100 |
wenzelm |
prefer local fixes;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:09:04 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Fri, 24 Oct 2014 15:07:51 +0200 |
hoelzl |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
file |
diff |
annotate
|
| Tue, 05 Aug 2014 16:58:19 +0200 |
wenzelm |
tuned proofs -- fewer warnings;
|
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
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Wed, 07 May 2014 12:25:35 +0200 |
hoelzl |
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
|
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:48 +0200 |
hoelzl |
field_simps: better support for negation and division, and power
|
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
|
| Wed, 02 Apr 2014 18:35:07 +0200 |
hoelzl |
extend continuous_intros; remove continuous_on_intros and isCont_intros
|
file |
diff |
annotate
|
| Wed, 02 Apr 2014 18:35:01 +0200 |
hoelzl |
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 09:39:07 -0700 |
huffman |
remove unnecessary finiteness assumptions from lemmas about setsum
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 10:12:58 +0100 |
immler |
removed dependencies on theory Ordered_Euclidean_Space
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 10:12:57 +0100 |
immler |
use cbox to relax class constraints
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 08:31:33 +0100 |
haftmann |
more complete set of lemmas wrt. image and composition
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 17:23:28 -0800 |
huffman |
remove lemmas in favor of more general ones: convex(_hull)_set_{plus,setsum}
|
file |
diff |
annotate
|
| Wed, 05 Mar 2014 16:57:00 -0800 |
huffman |
generalize lemma closure_sum
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 17:24:46 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sun, 23 Feb 2014 21:45:27 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
summarized notions related to ordered_euclidean_space and intervals in separate theory
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
prefer box over greaterThanLessThan on euclidean_space
|
file |
diff |
annotate
|
| Sun, 17 Nov 2013 21:46:12 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:02 +0100 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:58 +0100 |
hoelzl |
use bdd_above and bdd_below for conditionally complete lattices
|
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 18:09:17 -0700 |
huffman |
make 'linear' into a sublocale of 'bounded_linear';
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 17:36:37 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
file |
diff |
annotate
|
| Sat, 31 Aug 2013 22:18:51 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 31 Aug 2013 18:12:51 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 31 Aug 2013 00:39:59 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 18:22:17 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 00:11:01 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 19:59:19 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:57 +0100 |
hoelzl |
rename RealVector.thy to Real_Vector_Spaces.thy
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move connected to HOL image; used to show intermediate value theorem
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 20:31:22 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 18:46:52 +0100 |
wenzelm |
tuned proof -- much faster;
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 20:01:59 +0100 |
hoelzl |
generalized diameter from real_normed_vector to metric_space
|
file |
diff |
annotate
|
| Thu, 10 Jan 2013 14:40:19 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 15:46:01 +0100 |
hoelzl |
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
|
file |
diff |
annotate
|
| Fri, 16 Nov 2012 18:45:57 +0100 |
hoelzl |
move theorems to be more generally useable
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 20:38:42 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 20:37:47 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 22 Sep 2012 20:29:28 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 23:07:01 +0200 |
krauss |
Set_Algebras: removed syntax \<oplus> and \<otimes>, in favour of plain + and *
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 22:55:11 +0200 |
krauss |
removed "setsum_set", now subsumed by generic setsum
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 09:49:05 +0100 |
huffman |
avoid numeral-representation-specific rules in metis proof
|
file |
diff |
annotate
|
| Thu, 22 Sep 2011 14:12:16 -0700 |
huffman |
discontinued legacy theorem names from RealDef.thy
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 09:02:14 -0700 |
huffman |
modernize lemmas about 'continuous' and 'continuous_on';
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 13:51:22 -0700 |
huffman |
remove redundant lemma card_enum
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 19:41:38 -0700 |
huffman |
replace some continuous_on lemmas with more general versions
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 14:25:19 -0700 |
huffman |
generalize lemma finite_imp_compact_convex_hull and related lemmas
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 13:48:11 -0700 |
huffman |
generalize some lemmas
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 12:52:10 -0700 |
huffman |
generalize lemma convex_cone_hull
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 12:43:55 -0700 |
huffman |
rename subset_{interior,closure} to {interior,closure}_mono;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 09:17:02 -0700 |
huffman |
simplify definition of 'interior';
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 09:08:00 -0700 |
huffman |
change some subsection headings to subsubsection
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 16:47:48 -0700 |
huffman |
remove unnecessary lemma card_ge1
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 16:17:22 -0700 |
huffman |
move connected_real_lemma to the one place it is used
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 14:11:02 -0700 |
huffman |
declare euclidean_simps [simp] at the point they are proved;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 12:22:31 -0700 |
huffman |
add lemmas interior_Times and closure_Times
|
file |
diff |
annotate
|
| Sun, 21 Aug 2011 11:03:15 -0700 |
huffman |
remove unnecessary euclidean_space class constraints
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 15:54:26 -0700 |
huffman |
remove redundant lemma real_0_le_divide_iff in favor or zero_le_divide_iff
|
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
|
| Fri, 12 Aug 2011 09:17:24 -0700 |
huffman |
make Multivariate_Analysis work with separate set type
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 18:02:16 -0700 |
huffman |
avoid warnings about duplicate rules
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 08:42:26 -0700 |
huffman |
full import paths
|
file |
diff |
annotate
|
| Tue, 09 Aug 2011 10:30:00 -0700 |
huffman |
mark some redundant theorems as legacy
|
file |
diff |
annotate
|
| Sat, 30 Jul 2011 08:24:46 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 25 Jul 2011 23:26:55 +0200 |
haftmann |
adjusted to tailored version of ball_simps
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 00:36:01 +0100 |
hoelzl |
adapt proofs to changed set_plus_image (cf. ee8d0548c148);
|
file |
diff |
annotate
|
| Thu, 02 Dec 2010 16:45:28 +0100 |
hoelzl |
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 21:09:36 +0100 |
wenzelm |
keep private things private, without comments;
|
file |
diff |
annotate
|
| Fri, 05 Nov 2010 14:17:18 +0100 |
hoelzl |
Extend convex analysis by Bogdan Grechuk
|
file |
diff |
annotate
|
| 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
|
file |
diff |
annotate
|