| Wed, 11 Dec 2024 11:18:52 +0100 |
wenzelm |
proper bundle binomial_syntax;
|
file |
diff |
annotate
|
| Mon, 23 Sep 2024 13:32:38 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Sun, 12 May 2024 23:23:39 +0100 |
paulson |
syntax of gchoose now the same as choose
|
file |
diff |
annotate
|
| Mon, 06 May 2024 14:39:33 +0100 |
paulson |
Some new simprules – and patches for proofs
|
file |
diff |
annotate
|
| Wed, 07 Feb 2024 22:39:42 +0000 |
paulson |
Two new theorems
|
file |
diff |
annotate
|
| Fri, 02 Feb 2024 11:25:11 +0000 |
paulson |
A small number of new lemmas
|
file |
diff |
annotate
|
| Tue, 30 Jan 2024 16:39:21 +0000 |
paulson |
A few more new theorems taken from AFP entries
|
file |
diff |
annotate
|
| Fri, 15 Sep 2023 20:46:50 +0100 |
paulson |
A few more inclusion-exclusion theorems from HOL Light
|
file |
diff |
annotate
|
| Sat, 09 Sep 2023 19:26:08 +0100 |
paulson |
Loads of new material related to porting the Euler Polyhedron Formula from HOL Light
|
file |
diff |
annotate
|
| Wed, 01 Feb 2023 20:21:33 +0100 |
wenzelm |
isabelle update -u cite -l "";
|
file |
diff |
annotate
|
| Mon, 15 Aug 2022 12:50:24 +0100 |
paulson |
The same, without adding a new simprule
|
file |
diff |
annotate
|
| Sun, 14 Aug 2022 23:51:47 +0100 |
paulson |
moved some material from Sum_of_Powers
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 20:08:24 +0100 |
paulson |
The right way to formulate card_UNION, plus the old version for compatibility
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Fri, 25 Sep 2020 14:11:48 +0100 |
paulson |
fixed some remarkably ugly proofs
|
file |
diff |
annotate
|
| Mon, 06 Apr 2020 22:46:55 +0100 |
paulson |
removed more applys
|
file |
diff |
annotate
|
| Mon, 06 Apr 2020 19:46:38 +0100 |
paulson |
a few more applys
|
file |
diff |
annotate
|
| Tue, 07 Jan 2020 07:03:18 +0100 |
nipkow |
generalized thm (as suggested by Christian Weinz)
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 21:29:32 +0100 |
paulson |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 13:34:55 +0100 |
paulson |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 03 Oct 2018 09:46:42 +0200 |
nipkow |
shuffle -> shuffles
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 12:32:58 +0000 |
haftmann |
more uniform parameter naming convention for choose and gchoose
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 12:32:58 +0000 |
haftmann |
slightly generalized theorems
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 12:32:58 +0000 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Wed, 22 Aug 2018 12:32:58 +0000 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 03 May 2018 22:34:49 +0100 |
paulson |
Some tidying up (mostly regarding summations from 0)
|
file |
diff |
annotate
|
| Tue, 16 Jan 2018 09:30:00 +0100 |
wenzelm |
standardized towards new-style formal comments: isabelle update_comments;
|
file |
diff |
annotate
|
| Sat, 13 Jan 2018 09:18:54 +0000 |
haftmann |
restored naming of lemmas after corresponding constants
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Fri, 29 Dec 2017 19:17:52 +0100 |
wenzelm |
prefer formal citations;
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 09:30:09 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Fri, 12 May 2017 20:03:50 +0200 |
haftmann |
relaxed theory dependencies
|
file |
diff |
annotate
|
| Fri, 12 May 2017 07:53:35 +0200 |
haftmann |
explicit theory for factorials
|
file |
diff |
annotate
|
| Wed, 26 Apr 2017 13:41:32 +0200 |
eberlm |
better code equation for binomial
|
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
|
| Mon, 03 Apr 2017 16:56:45 +0200 |
eberlm |
added shuffle product to HOL/List
|
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
|
| 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
|
| Mon, 02 Nov 2015 11:56:28 +0100 |
eberlm |
Rounding function, uniform limits, cotangent, binomial identities
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 16 Jun 2015 11:31:22 +0200 |
hoelzl |
tuned src/HOL/ex/Ballot
|
file |
diff |
annotate
|
| Mon, 25 May 2015 22:11:43 +0200 |
wenzelm |
merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 16:45:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Apr 2015 17:19:00 +0100 |
paulson |
New material, mostly about limits. Consolidation.
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 21:54:32 +0200 |
haftmann |
given up separate type classes demanding `inverse 0 = 0`
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 15:00:03 +0100 |
paulson |
New material and binomial fix
|
file |
diff |
annotate
|
| Tue, 17 Mar 2015 15:11:25 +0000 |
paulson |
more general type class for factorial. Now allows code generation (?)
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 15:30:00 +0000 |
paulson |
The factorial function, "fact", now has type "nat => 'a"
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 16:12:35 +0000 |
paulson |
renaming HOL/Fact.thy -> Binomial.thy
|
file |
diff |
annotate
| base
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 10:04:27 +0100 |
ballarin |
Renamed setsum_mult to setsum_right_distrib.
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:03:37 +0200 |
wenzelm |
tuned theory dependencies;
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:36:56 +0200 |
nipkow |
Used to be part of Finite_Set (or was it SetInterval?)
|
file |
diff |
annotate
|