| Tue, 02 May 2017 14:34:06 +0100 |
paulson |
Simplification of some proofs. Also key lemmas using !! rather than ! in premises
|
file |
diff |
annotate
|
| Wed, 26 Apr 2017 15:53:35 +0100 |
paulson |
Further new material. The simprule status of some exp and ln identities was reverted.
|
file |
diff |
annotate
|
| Tue, 25 Apr 2017 16:39:54 +0100 |
paulson |
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
|
file |
diff |
annotate
|
| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2017 23:16:40 +0100 |
immler |
modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas
|
file |
diff |
annotate
|
| Sun, 05 Mar 2017 10:57:51 +0100 |
nipkow |
added numeral_powr_numeral
|
file |
diff |
annotate
|
| Mon, 27 Feb 2017 17:17:26 +0000 |
paulson |
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
|
file |
diff |
annotate
|
| Tue, 21 Feb 2017 15:04:01 +0000 |
paulson |
Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion
|
file |
diff |
annotate
|
| Tue, 03 Jan 2017 16:48:49 +0000 |
paulson |
A few new lemmas and needed adaptations
|
file |
diff |
annotate
|
| Tue, 22 Nov 2016 16:22:05 +0100 |
nipkow |
added simp rule
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 00:14:44 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2016 11:53:07 +0200 |
Manuel Eberl |
Some facts about factorial and binomial coefficients
|
file |
diff |
annotate
|
| Thu, 25 Aug 2016 15:50:43 +0200 |
Manuel Eberl |
More analysis lemmas
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 20:34:07 +0200 |
wenzelm |
more accurate cong del;
|
file |
diff |
annotate
|
| Thu, 28 Jul 2016 20:39:46 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Fri, 22 Jul 2016 11:00:43 +0200 |
wenzelm |
tuned proofs -- avoid unstructured calculation;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 22:54:37 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sat, 09 Jul 2016 13:26:16 +0200 |
haftmann |
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 20:22:25 +0200 |
haftmann |
simplified definitions of combinatorial functions
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
more theorems
|
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 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Wed, 25 May 2016 11:49:40 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
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
|
| Tue, 12 Apr 2016 11:18:29 +0200 |
immler |
added derivative of scaling in exponential function
|
file |
diff |
annotate
|
| Mon, 11 Apr 2016 16:27:42 +0100 |
paulson |
lots of new theorems for multivariate analysis
|
file |
diff |
annotate
|
| Mon, 21 Mar 2016 11:54:45 +0100 |
hoelzl |
add le_log_of_power and le_log2_of_power by Tobias Nipkow
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 18:04:31 +0100 |
nipkow |
resolved conflict
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 15:47:39 +0000 |
paulson |
New and revised material for (multivariate) analysis
|
file |
diff |
annotate
|
| Mon, 22 Feb 2016 14:37:56 +0000 |
paulson |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
generalized some lemmas;
|
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
|
| Mon, 28 Dec 2015 01:26:34 +0100 |
wenzelm |
prefer symbols for "abs";
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 21:46:36 +0100 |
wenzelm |
prefer symbols for "floor", "ceiling";
|
file |
diff |
annotate
|
| Mon, 21 Dec 2015 14:44:44 +0100 |
hoelzl |
Transcendental: use [simp]-canonical form - (pi/2)
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 17:35:22 +0000 |
paulson |
sorted out eventually_mono
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +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
|
| Fri, 13 Nov 2015 12:27:13 +0000 |
paulson |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
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 16:17:09 +0100 |
eberlm |
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
|
file |
diff |
annotate
|
| Mon, 02 Nov 2015 11:56:28 +0100 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
| Thu, 29 Oct 2015 15:40:52 +0100 |
eberlm |
added many small lemmas about setsum/setprod/powr/...
|
file |
diff |
annotate
|
| Mon, 26 Oct 2015 23:41:27 +0000 |
paulson |
new lemmas about topology, etc., for Cauchy integral formula
|
file |
diff |
annotate
|
| Wed, 30 Sep 2015 16:36:42 +0100 |
paulson |
real_of_nat_Suc is now a simprule
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 21:28:08 +0200 |
wenzelm |
prefer symbols;
|
file |
diff |
annotate
|
| Thu, 06 Aug 2015 23:56:48 +0200 |
haftmann |
slight cleanup of lemmas
|
file |
diff |
annotate
|
| Mon, 20 Jul 2015 23:12:50 +0100 |
paulson |
new material for multivariate analysis, etc.
|
file |
diff |
annotate
|