| Tue, 18 Oct 2016 12:01:54 +0200 |
hoelzl |
HOL-Analysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
|
file |
diff |
annotate
|
| Thu, 13 Oct 2016 18:36:06 +0200 |
hoelzl |
HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
|
file |
diff |
annotate
|
| Fri, 30 Sep 2016 16:08:38 +0200 |
hoelzl |
HOL-Probability: more about probability, prepare for Markov processes in the AFP
|
file |
diff |
annotate
|
| Wed, 28 Sep 2016 17:01:01 +0100 |
paulson |
new material connected with HOL Light measure theory, plus more rationalisation
|
file |
diff |
annotate
|
| Wed, 17 Aug 2016 16:16:38 +0200 |
eberlm |
Tuned L'Hospital
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 11:26:36 +0200 |
wenzelm |
proper latex;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 11:07:51 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Wed, 15 Jun 2016 22:19:03 +0200 |
hoelzl |
move open_Collect_eq/less to HOL
|
file |
diff |
annotate
|
| Thu, 16 Jun 2016 17:57:09 +0200 |
eberlm |
Various additions to polynomials, FPSs, Gamma function
|
file |
diff |
annotate
|
| Tue, 14 Jun 2016 15:34:21 +0100 |
paulson |
new results about topology
|
file |
diff |
annotate
|
| Mon, 13 Jun 2016 15:23:12 +0200 |
eberlm |
Facts about HK integration, complex powers, Gamma function
|
file |
diff |
annotate
|
| Fri, 27 May 2016 23:35:13 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
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
|
| Mon, 04 Apr 2016 16:52:56 +0100 |
paulson |
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 14:34:45 +0000 |
paulson |
new material to Blochj's theorem, as well as supporting lemmas
|
file |
diff |
annotate
|
| Wed, 24 Feb 2016 15:51:01 +0000 |
paulson |
Substantial new material for multivariate analysis. Also removal of some duplicates.
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 15:47:39 +0000 |
paulson |
New and revised material for (multivariate) analysis
|
file |
diff |
annotate
|
| Tue, 09 Feb 2016 06:39:31 +0100 |
hoelzl |
instantiate topologies for nat, int and enat
|
file |
diff |
annotate
|
| Mon, 08 Feb 2016 17:18:13 +0100 |
hoelzl |
move product topology to HOL-Complex_Main
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Fri, 22 Jan 2016 16:00:03 +0000 |
paulson |
Reorganised a huge proof
|
file |
diff |
annotate
|
| Wed, 13 Jan 2016 23:07:06 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Mon, 11 Jan 2016 11:56:35 +0100 |
hoelzl |
setup code generation for filters as suggested by Florian
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 17:41:04 +0100 |
hoelzl |
fix code generation for uniformity: uniformity is a non-computable pure data.
|
file |
diff |
annotate
|
| Fri, 08 Jan 2016 17:40:59 +0100 |
hoelzl |
add uniform spaces
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 12:18:53 +0100 |
hoelzl |
add the proof of the central limit theorem
|
file |
diff |
annotate
|
| Mon, 04 Jan 2016 17:45:36 +0100 |
eberlm |
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 14:05:51 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 30 Dec 2015 11:21:54 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 29 Dec 2015 23:04:53 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 22 Dec 2015 14:33:34 +0000 |
paulson |
Liouville theorem, Fundamental Theorem of Algebra, etc.
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 16:44:26 +0000 |
paulson |
Cauchy's integral formula for circles. Starting to fix eventually_mono.
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
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
|
| 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
|
| 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
|
| Tue, 06 Oct 2015 17:46:07 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 02 Oct 2015 15:07:41 +0100 |
paulson |
New theorems about connected sets. And pairwise moved to Set.thy.
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 16:54:31 +0200 |
hoelzl |
prove Liminf_inverse_ereal
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 16:55:07 +0100 |
paulson |
New lemmas
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 19:52:13 +0100 |
paulson |
new lemmas and movement of lemmas into place
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Mon, 20 Jul 2015 23:12:50 +0100 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 14 Jul 2015 13:37:44 +0200 |
hoelzl |
add continuous_onI_mono
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 10:20:33 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 07 May 2015 15:34:28 +0200 |
hoelzl |
generalized tends over powr; added DERIV rule for powr
|
file |
diff |
annotate
|
| Mon, 04 May 2015 17:35:31 +0200 |
hoelzl |
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
|
file |
diff |
annotate
|
| Tue, 28 Apr 2015 16:23:38 +0100 |
paulson |
New material about complex transcendental functions (especially Ln, Arg) and polynomials
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:34:09 +0200 |
hoelzl |
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
|
file |
diff |
annotate
|
| Sun, 12 Apr 2015 11:33:19 +0200 |
hoelzl |
move filters to their own theory
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 21:42:08 +0200 |
wenzelm |
more standard access to goal state;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:58:52 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|