| 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
|
| Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| Mon, 19 Sep 2016 20:06:21 +0200 |
fleury |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 11:48:20 +0200 |
nipkow |
renamed listsum -> sum_list, listprod ~> prod_list
|
file |
diff |
annotate
|
| Fri, 26 Aug 2016 11:58:19 +0200 |
Manuel Eberl |
Bohr-Mollerup theorem for the Gamma function
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 09:33:54 +0200 |
nipkow |
"split add" -> "split"
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 11:11:07 +0200 |
wenzelm |
unused (see also 651ea265d568);
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 21:53:56 +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
|
| Mon, 04 Jul 2016 19:46:19 +0200 |
haftmann |
tuned sections
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 19:46:19 +0200 |
haftmann |
relating gbinomial and binomial, still using distinct definitions
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 20:22:25 +0200 |
haftmann |
simplified definitions of combinatorial functions
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 15:02:24 +0200 |
haftmann |
define binomial coefficents directly via combinatorial definition
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
more correct comment
|
file |
diff |
annotate
|
| Thu, 16 Jun 2016 17:57:09 +0200 |
eberlm |
Various additions to polynomials, FPSs, Gamma function
|
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, 01 Mar 2016 10:36:19 +0100 |
haftmann |
tuned bootstrap order to provide type classes in a more sensible order
|
file |
diff |
annotate
|
| Fri, 19 Feb 2016 13:40:50 +0100 |
hoelzl |
generalize more theorems to support enat and ennreal
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
|
file |
diff |
annotate
|
| Tue, 12 Jan 2016 16:59:32 +0100 |
eberlm |
Deleted problematic code equation in Binomial temporarily.
|
file |
diff |
annotate
|
| Mon, 11 Jan 2016 16:38:39 +0100 |
eberlm |
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
|
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
|
| 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, 03 Nov 2015 15:24:24 +0100 |
eberlm |
added acknowledgement in Binomial.thy
|
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
|