| Sat, 15 Jul 2017 14:54:13 +0100 |
eberlm |
Simprocs for roots of numerals
|
file |
diff |
annotate
|
| 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
|