#
a9ab1fba |
|
06-Jan-2020 |
nipkow <none@none> |
generalized thm (as suggested by Christian Weinz)
|
#
35216754 |
|
10-Apr-2019 |
paulson <lp15@cam.ac.uk> |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
#
48a391b7 |
|
10-Apr-2019 |
paulson <lp15@cam.ac.uk> |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
#
e977f1fa |
|
31-Jan-2019 |
haftmann <none@none> |
proper congruence rule for image operator --HG-- extra : rebase_source : 71f59936260619419f4d3f7f86d1b930bc771065
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
9e188bc2 |
|
03-Oct-2018 |
nipkow <none@none> |
shuffle -> shuffles
|
#
cc37beb1 |
|
24-Sep-2018 |
nipkow <none@none> |
Prefix form of infix with * on either side no longer needs special treatment because (* and *) are no longer comment brackets in terms.
|
#
6920d5d3 |
|
21-Aug-2018 |
haftmann <none@none> |
more uniform parameter naming convention for choose and gchoose --HG-- extra : rebase_source : 9635a3976a30f3bb8ea5c228cef6be401bf6a444
|
#
88ce38b5 |
|
21-Aug-2018 |
haftmann <none@none> |
slightly generalized theorems --HG-- extra : rebase_source : 39c09f24eaa09333fd525f70a11d02d0f6d3b293
|
#
e0859e83 |
|
21-Aug-2018 |
haftmann <none@none> |
tuned code setup --HG-- extra : rebase_source : 2aabfdd7092cf79ea3a20b77459c3d91eae96ec7
|
#
a291e832 |
|
21-Aug-2018 |
haftmann <none@none> |
tuned --HG-- extra : rebase_source : dc4b091146718b1add2d5f71ff97a9117c8371a4
|
#
48745e07 |
|
03-May-2018 |
paulson <lp15@cam.ac.uk> |
Some tidying up (mostly regarding summations from 0)
|
#
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
#
fa1f0d8b |
|
13-Jan-2018 |
haftmann <none@none> |
restored naming of lemmas after corresponding constants
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
9ce7e848 |
|
29-Dec-2017 |
wenzelm <none@none> |
prefer formal citations; more accurate bibtex entries;
|
#
2ef94418 |
|
08-Oct-2017 |
haftmann <none@none> |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel --HG-- extra : rebase_source : c6612d6016d811043143eafb7a671631287494a1
|
#
eee6992c |
|
03-Aug-2017 |
nipkow <none@none> |
added lemmas
|
#
8d131b79 |
|
12-May-2017 |
haftmann <none@none> |
relaxed theory dependencies
|
#
a7795d49 |
|
11-May-2017 |
haftmann <none@none> |
explicit theory for factorials --HG-- extra : rebase_source : 1d0d73d3b93f0eb079a100628954fb1688def32f
|
#
85ab1a42 |
|
26-Apr-2017 |
eberlm <eberlm@in.tum.de> |
better code equation for binomial
|
#
3f30d088 |
|
22-Apr-2017 |
wenzelm <none@none> |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications; --HG-- rename : src/HOL/Main.thy => src/HOL/Pre_Main.thy
|
#
bc83a162 |
|
03-Apr-2017 |
eberlm <eberlm@in.tum.de> |
added shuffle product to HOL/List --HG-- extra : amend_source : f69971cd7b125b625e2945b41373d36d943083aa
|
#
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
#
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
#
7cb68da2 |
|
16-Oct-2016 |
haftmann <none@none> |
more standardized names
|
#
9a8c3fb3 |
|
19-Sep-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
left_distrib ~> distrib_right, right_distrib ~> distrib_left
|
#
131dfaff |
|
15-Sep-2016 |
nipkow <none@none> |
renamed listsum -> sum_list, listprod ~> prod_list
|
#
b662a405 |
|
26-Aug-2016 |
Manuel Eberl <eberlm@in.tum.de> |
Bohr-Mollerup theorem for the Gamma function
|
#
9b9c2176 |
|
12-Aug-2016 |
wenzelm <none@none> |
more symbols;
|
#
2df4ddef |
|
10-Aug-2016 |
nipkow <none@none> |
"split add" -> "split"
|
#
558a6dd5 |
|
20-Jul-2016 |
wenzelm <none@none> |
unused (see also 651ea265d568);
|
#
417877bb |
|
12-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
a70bd0e1 |
|
09-Jul-2016 |
haftmann <none@none> |
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat * * * more rules for setsum, setprod on intervals
|
#
56b0b265 |
|
04-Jul-2016 |
haftmann <none@none> |
tuned sections
|
#
c1f0c688 |
|
04-Jul-2016 |
haftmann <none@none> |
relating gbinomial and binomial, still using distinct definitions
|
#
b1935b2f |
|
02-Jul-2016 |
haftmann <none@none> |
simplified definitions of combinatorial functions
|
#
0a0d0b0c |
|
02-Jul-2016 |
haftmann <none@none> |
define binomial coefficents directly via combinatorial definition
|
#
768bd21a |
|
02-Jul-2016 |
haftmann <none@none> |
more correct comment
|
#
1e23b491 |
|
16-Jun-2016 |
eberlm <none@none> |
Various additions to polynomials, FPSs, Gamma function
|
#
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
#
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def'; tuned comments;
|
#
70cb89b7 |
|
01-Mar-2016 |
haftmann <none@none> |
tuned bootstrap order to provide type classes in a more sensible order --HG-- extra : rebase_source : b4008b5f377525bc1866d515a16702fbb0b463c9
|
#
3a51760b |
|
19-Feb-2016 |
hoelzl <none@none> |
generalize more theorems to support enat and ennreal --HG-- extra : rebase_source : 11176604a37483aa41462153f0aa289df506590d
|
#
a6f23363 |
|
17-Feb-2016 |
haftmann <none@none> |
generalized some lemmas; moved some lemmas in more appropriate places; deleted potentially dangerous simp rule
|
#
9b9ee20c |
|
17-Feb-2016 |
haftmann <none@none> |
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
|
#
4fdeee21 |
|
12-Jan-2016 |
eberlm <none@none> |
Deleted problematic code equation in Binomial temporarily.
|
#
e89ec887 |
|
11-Jan-2016 |
eberlm <none@none> |
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
3dc932ef |
|
23-Nov-2015 |
paulson <lp15@cam.ac.uk> |
New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.
|
#
420aaf4c |
|
12-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
#
6bac7927 |
|
03-Nov-2015 |
eberlm <none@none> |
added acknowledgement in Binomial.thy
|
#
dbea1757 |
|
02-Nov-2015 |
eberlm <none@none> |
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
|
#
dd88f1ec |
|
02-Nov-2015 |
eberlm <none@none> |
Rounding function, uniform limits, cotangent, binomial identities
|
#
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
04a37fd5 |
|
16-Jun-2015 |
hoelzl <none@none> |
tuned src/HOL/ex/Ballot
|
#
7c42725f |
|
03-May-2015 |
wenzelm <none@none> |
tuned;
|
#
cd8a26ec |
|
21-Apr-2015 |
paulson <lp15@cam.ac.uk> |
New material, mostly about limits. Consolidation.
|
#
ac517014 |
|
31-Mar-2015 |
haftmann <none@none> |
given up separate type classes demanding `inverse 0 = 0`
|
#
7416c0a5 |
|
31-Mar-2015 |
paulson <lp15@cam.ac.uk> |
New material and binomial fix
|
#
6fc6fa5f |
|
17-Mar-2015 |
paulson <lp15@cam.ac.uk> |
more general type class for factorial. Now allows code generation (?)
|
#
3e14dd10 |
|
16-Mar-2015 |
paulson <lp15@cam.ac.uk> |
The factorial function, "fact", now has type "nat => 'a"
|
#
b9259bee |
|
10-Mar-2015 |
paulson <lp15@cam.ac.uk> |
renaming HOL/Fact.thy -> Binomial.thy --HG-- rename : src/HOL/Fact.thy => src/HOL/Binomial.thy
|
#
745db1a3 |
|
26-Jul-2006 |
webertj <none@none> |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
#
ba4ed7ee |
|
17-Mar-2006 |
ballarin <none@none> |
Renamed setsum_mult to setsum_right_distrib.
|
#
112ea486 |
|
20-Sep-2005 |
wenzelm <none@none> |
tuned theory dependencies;
|
#
2f83306c |
|
06-Jul-2005 |
nipkow <none@none> |
Used to be part of Finite_Set (or was it SetInterval?) Added binomial thm.
|