generalized thm (as suggested by Christian Weinz)

Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context

The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale

proper congruence rule for image operator

--HG--
extra : rebase_source : 71f59936260619419f4d3f7f86d1b930bc771065

isabelle update -u control_cartouches;

shuffle -> shuffles

Prefix form of infix with * on either side no longer needs special treatment
because (* and *) are no longer comment brackets in terms.

more uniform parameter naming convention for choose and gchoose

--HG--
extra : rebase_source : 9635a3976a30f3bb8ea5c228cef6be401bf6a444

slightly generalized theorems

--HG--
extra : rebase_source : 39c09f24eaa09333fd525f70a11d02d0f6d3b293

tuned code setup

--HG--
extra : rebase_source : 2aabfdd7092cf79ea3a20b77459c3d91eae96ec7

tuned

--HG--
extra : rebase_source : dc4b091146718b1add2d5f71ff97a9117c8371a4

Some tidying up (mostly regarding summations from 0)

standardized towards new-style formal comments: isabelle update_comments;

restored naming of lemmas after corresponding constants

ran isabelle update_op on all sources

prefer formal citations;
more accurate bibtex entries;

abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel

--HG--
extra : rebase_source : c6612d6016d811043143eafb7a671631287494a1

added lemmas

relaxed theory dependencies

explicit theory for factorials

--HG--
extra : rebase_source : 1d0d73d3b93f0eb079a100628954fb1688def32f

better code equation for binomial

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

added shuffle product to HOL/List

--HG--
extra : amend_source : f69971cd7b125b625e2945b41373d36d943083aa

setprod -> prod

setsum -> sum

more standardized names

left_distrib ~> distrib_right, right_distrib ~> distrib_left

renamed listsum -> sum_list, listprod ~> prod_list

Bohr-Mollerup theorem for the Gamma function

more symbols;

"split add" -> "split"

unused (see also 651ea265d568);

misc tuning and modernization;

more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
* * *
more rules for setsum, setprod on intervals

tuned sections

relating gbinomial and binomial, still using distinct definitions

simplified definitions of combinatorial functions

define binomial coefficents directly via combinatorial definition

more correct comment

Various additions to polynomials, FPSs, Gamma function

eliminated use of empty "assms";

eliminated old 'def';
tuned comments;

tuned bootstrap order to provide type classes in a more sensible order

--HG--
extra : rebase_source : b4008b5f377525bc1866d515a16702fbb0b463c9

generalize more theorems to support enat and ennreal

--HG--
extra : rebase_source : 11176604a37483aa41462153f0aa289df506590d

generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule

pulled out legacy aliasses and infamous dvd interpretations into theory appendix

Deleted problematic code equation in Binomial temporarily.

Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.

isabelle update_cartouches -c -t;

New material about paths, winding numbers, etc. Added lemmas to divide_const_simps. Misc tuning.

Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.

added acknowledgement in Binomial.thy

Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer

Rounding function, uniform limits, cotangent, binomial identities

eliminated \<Colon>;

isabelle update_cartouches;

tuned src/HOL/ex/Ballot

tuned;

New material, mostly about limits. Consolidation.

given up separate type classes demanding `inverse 0 = 0`

New material and binomial fix

more general type class for factorial. Now allows code generation (?)

The factorial function, "fact", now has type "nat => 'a"

renaming HOL/Fact.thy -> Binomial.thy

--HG--
rename : src/HOL/Fact.thy => src/HOL/Binomial.thy

linear arithmetic splits certain operators (e.g. min, max, abs)

Renamed setsum_mult to setsum_right_distrib.

tuned theory dependencies;

Used to be part of Finite_Set (or was it SetInterval?)
Added binomial thm.