de-applying (mostly Set_Interval)

infinite product material

type class generalisations; some work on infinite products

more and generalized lemmas

--HG--
extra : rebase_source : 427f9ca2975f1d4f8635e3509a6d1045335cf09a

prefer convention to place operation name before type name

abstract algebraic bit operations

--HG--
extra : rebase_source : 10402190e8858b0ea47b7ac7f91671a9935921ae

moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements

moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations

more symbols;

standardized towards new-style formal comments: isabelle update_comments;

restored naming of lemmas after corresponding constants

ran isabelle update_op on all sources

more symbols;

tuned some proofs and added some lemmas

--HG--
extra : rebase_source : ad93f195ceb7a124396a911453e61f00f52999be

tuned imports

--HG--
extra : rebase_source : bc9797cb892085195c2d8662a7ca3896dd1e5011

added lemma

New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series

Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.

Many new theorems, and more tidying

setprod -> prod

setsum -> sum

new material on paths, etc. Also rationalisation

raw control symbols are superseded by Latex.embed_raw;

left_distrib ~> distrib_right, right_distrib ~> distrib_left

tuned proofs;

simple new lemmas, mostly about sets

More analysis lemmas

tuned proofs -- avoid unstructured calculation;

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

more theorems

Various additions to polynomials, FPSs, Gamma function

tuned proofs;

Lots of new material for multivariate analysis

Moved material from AFP/Randomised_Social_Choice to distribution

eliminated use of empty "assms";

explicit property for unbreakable block;

more canonical names

An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!

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

instantiate topologies for nat, int and enat

--HG--
extra : rebase_source : 2320da44d4913f441c671ef425945fac6d4381c9

prefer abbreviations for compound operators INFIMUM and SUPREMUM

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

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

isabelle update_cartouches -c -t;

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

discontinued specific HTML syntax;

new lemmas and movement of lemmas into place

the Cauchy integral theorem and related material

new material for multivariate analysis, etc.

isabelle update_cartouches;

Useful lemmas. The theorem concerning swapping the variables in a double integral.

proper spacing, as for other syntax for these symbols;

tidying some messy proofs

New material about complex transcendental functions (especially Ln, Arg) and polynomials

Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.

generalized sum_diff_distrib to setsum_subtractf_nat

--HG--
extra : rebase_source : 713d89f4f5743dee1259a32a3ec3dc08984cd6bf

import general theorems from AFP/Markov_Models

add forgotten lemma

modernized header uniformly as section;

prefer ac_simps collections over separate name bindings for add and mult

reduced name variants for assoc and commute on plus and mult

more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs

--HG--
extra : rebase_source : 8664c1d86ed72607199cc8197a480070514ae330

import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure

--HG--
extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141

fact consolidation

introduce more powerful reindexing rules for big operators

New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)

clean up Lebesgue integration

field_simps: better support for negation and division, and power

add rules about infinity of intervals

a few new lemmas and generalisations of old ones

New complex analysis material

fix HOL-NSA; move lemmas

cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}

Lemmas about Reals, norm, etc., and cleaner variants of existing ones

A few lemmas about summations, etc.

Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.

explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;

moved 'bacc' back to 'Enum' (cf. 744934b818c7) -- reduces baggage loaded by 'Hilbert_Choice'

moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain

--HG--
rename : src/HOL/FunDef.thy => src/HOL/Fun_Def.thy

cleaned up indirect dependency

killed most "no_atp", to make Sledgehammer more complete

tuned proofs -- clarified flow of facts wrt. calculation;

renamed inner_dense_linorder to dense_linorder

--HG--
extra : rebase_source : a7a9c602f6d7437d9632ccdffa7d3b6eaafc2d01

factored syntactic type classes for bot and top (by Alessandro Coglio)

lifting for primitive definitions;
explicit conversions from and to lists of coefficients, used for generated code;
replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions;
prefer pre-existing gcd operation for gcd

more lemmas about intervals

split dense into inner_dense_order and no_top/no_bot

move auxiliary lemmas from Library/Extended_Reals to HOL image

added lemma

introduce order topology

add Int_atMost

tuned proofs;

modernized obsolete old-style theory name with proper new-style underscore

--HG--
rename : src/HOL/SetInterval.thy => src/HOL/Set_Interval.thy