added lemma

imported new material mostly due to Sébastien Gouëzel

merge plus tidied three proofs

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

fixed markup in Poly_Mapping; Free_Abelian_Groups (but not yet imported by Algebra!)

More group theory. Sum and product indexed by the non-neutral part of a set

removed subsumed lemma

less special syntax: make \<Sum> an ordinary function symbol

new material about summations and powers, along with some tweaks

uniform naming

isabelle update -u control_cartouches;

generalized to big sum

Retired lemma card_Union_image; use the simpler card_UN_disjoint instead.

clarified status of legacy input abbreviations

uniform naming of strong congruence rules

new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml

generalization due to Alexander Maletzky

A few new results, elimination of duplicates and more use of "pairwise"

infinite product material

Syntax for the special cases Min(A`I) and Max (A`I)

Lots of new material about matrices, etc.

lots of new material, ultimately related to measure theory

include lemmas generally useful for combinatorial proofs

new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product

tuned some proofs and added some lemmas

--HG--
extra : rebase_source : ad93f195ceb7a124396a911453e61f00f52999be

avoid name clashes on interpretation of abstract locales

--HG--
extra : rebase_source : f524b077cafad9e920061f751ff3126d7a903434

tuning imports

New theorems; stronger theorems; tidier theorems. Also some renaming

Some new material. SIMPRULE STATUS for sum/prod.delta rules!

two new theorems

Simplification of some proofs. Also key lemmas using !! rather than ! in premises

move mono_neutral_cong from AFP/Deep_Learning/PP_Auxiliary

setprod -> prod

setsum -> sum

new material connected with HOL Light measure theory, plus more rationalisation

More mainly topological results

more generic algebraic lemmas

--HG--
extra : rebase_source : afd1b38644ce9418dc6eeaf977c35a8502e396b5

left_distrib ~> distrib_right, right_distrib ~> distrib_left

tuned proofs;

misc tuning and modernization;

add lemmas contributed by Peter Gammie

added fundef_cong rule

boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes

--HG--
extra : rebase_source : 4542f54b0b7fe6c0bea5be2116706e4cfacadaf0

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

moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add

--HG--
extra : rebase_source : 8674c79985a670cee921b8193965bb0767549a5c

Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.

--HG--
extra : rebase_source : 54bd3e5fcde04ef38241be91231c48d078b850f2

former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";

prefer symbols for "Union", "Inter";

prefer symbols for "abs";

discontinued ASCII replacement syntax <*>;

isabelle update_cartouches -c -t;

modernized

qualifier is mandatory by default;

Keyword 'rewrites' identifies rewrite morphisms.

added many small lemmas about setsum/setprod/powr/...

discontinued specific HTML syntax;

tuned proofs -- less legacy;

standardized some occurences of ancient "split" alias

--HG--
extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5

New material and fixes related to the forthcoming Stone-Weierstrass development

isabelle update_cartouches;

correccted the pretty-printing specs for setsum and setprod

uniform _ div _ as infix syntax for ring division

--HG--
extra : rebase_source : c4a1892078772c7ce9af33ad66e2abfefe7adea9

implicit partial divison operation in integral domains

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

clarified no_zero_devisors: makes only sense in a semiring;
actually turn linorder_semidom into a integral domain

--HG--
extra : rebase_source : 20e224f329987c38e10dba58521b744a19110ced

A few new lemmas and a bit of tidying up

generalized sum_diff_distrib to setsum_subtractf_nat

--HG--
extra : rebase_source : 713d89f4f5743dee1259a32a3ec3dc08984cd6bf

generalized lemmas and tuned proofs

modernized header uniformly as section;

added lemma

added various facts

added lemmas

--HG--
extra : rebase_source : 9983f0122781b2719b4390818c18fedd04f9cbb5

reduced name variants for assoc and commute on plus and mult

fact consolidation

moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin

--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2

introduce more powerful reindexing rules for big operators

more operations and lemmas

--HG--
extra : rebase_source : 8f5be7e0cdc09c667e66c2cda2c667d4da6e5f73

made mult_pos_pos a simp rule

made mult_nonneg_nonneg a simp rule

--HG--
extra : rebase_source : 3f70ac991fa0f02839309ce9b8f418ff53f87c36

normalising simp rules for compound operators

removed theory dependency of BNF_LFP on Datatype

disambiguation of interpretation prefixes

more algebraic terminology for theories about big operators