de-applying and removing junk

de-applying

de-applying

Incorporating new/strengthened proofs from Library and AFP entries

Rationalisation of complex transcendentals, esp the Arg function

New material in support of quaternions

isabelle update_comments;

added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly

--HG--
rename : src/HOL/Library/FuncSet.thy => src/HOL/FuncSet.thy

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

Unified the order of zeros and poles; improved reasoning around non-essential singularites

--HG--
extra : amend_source : 528e99138923389ffcb3b2021c959a3c9f20de52

lots of new material, ultimately related to measure theory

ran isabelle update_op on all sources

Moved material from AFP to Analysis/Number_Theory

--HG--
extra : amend_source : 77bbfc2e280a37511c491c48def2d0c01459e12c

new material about connectedness, etc.

patching the previous commit

further Hensock tidy-up

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

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

Further new material. The simprule status of some exp and ln identities was reverted.

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

Some new lemmas. Existing lemmas modified to use uniform_limit rather than its expansion

New material about path connectedness, etc.

setprod -> prod

setsum -> sum

more standardized names

new material on paths, etc. Also rationalisation

vector_add_divide_simps now a "named theorems" bundle

tuned proofs;

more symbols;

numerical bounds on pi

misc tuning and modernization;

lots of new theorems about differentiable_on, retracts, ANRs, etc.

renamings and new material

Lots of new material for multivariate analysis

eliminated old 'def';
tuned comments;

lots of new theorems for multivariate analysis

rationalisation of theorem names esp about "real Archimedian" etc.

new material to Blochj's theorem, as well as supporting lemmas

Substantial new material for multivariate analysis. Also removal of some duplicates.

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

add type class for topological monoids

--HG--
extra : rebase_source : bedca3d32972c3f447e37ac5aac3de5ac763b94b

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

nonneg_Reals, nonpos_Reals, Cauchy integral formula, etc.

fix code generation for uniformity: uniformity is a non-computable pure data.

add uniform spaces

revisions to limits and derivatives, plus new lemmas

Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function

more symbols;

more symbols;

more symbols;

prefer symbols for "floor", "ceiling";

transfer rule for bounded_linear of blinfun

theory for type of bounded linear functions; differentiation under the integral sign

isabelle update_cartouches -c -t;

Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.

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

Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.

Rounding function, uniform limits, cotangent, binomial identities

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

tuned proofs -- less legacy;

prefer symbols;

New material for Cauchy's integral theorem

new material for multivariate analysis, etc.

isabelle update_cartouches;

Convex hulls: theorems about interior, etc. And a few simple lemmas.

New material about paths, and some lemmas

Tidying. Improved simplification for numerals, esp in exponents.

Restored LIMSEQ_def as legacy binding. [The other changes are whitespace only.]

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

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

Lots of new material on complex-valued functions. Modified simplification of (x/n)^k

sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex

The function frac. Various lemmas about limits, series, the exp function, etc.

Removed the obsolete functions "natfloor" and "natceiling"

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

fact consolidation

filters are easier to define with INF on filters.

--HG--
extra : rebase_source : 5626307315d6be224d16a97b9160690f09c8e0d4

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

--HG--
extra : rebase_source : cd4a9d91f2d415deaa6fd3411b5402ef770d74d2

avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.

--HG--
extra : rebase_source : 899541490c73fe6897445f97dc2a5a3c929cf153

revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules

removing simprule status for divide_minus_left and divide_minus_right

moved generic theorems from Complex_Analysis_Basic; fixed some theorem names

fix HOL-NSA; move lemmas

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

fundamental treatment of undefined vs. universally partial replaces code_abort

prefer more canonical names for lemmas on min/max

lemmas about divideR and scaleR

introduced ordered real vector spaces

more antiquotations;

eliminiated neg_numeral in favour of - (numeral _)

move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)

--HG--
rename : src/HOL/Library/Glbs.thy => src/HOL/Library/Lubs_Glbs.thy

more simplification rules on unary and binary minus

--HG--
extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1

make 'linear' into a sublocale of 'bounded_linear';
replace 'linear_def' with 'linear_iff'

tuned proofs -- less guessing;

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

pragmatic executability for instance real :: open

revert #916271d52466; add non-topological linear_continuum type class; show linear_continuum_topology is a perfect_space

renamed linear_continuum_topology to connected_linorder_topology (and mention in NEWS)

--HG--
extra : rebase_source : 63f5230a997c030fcaa8377e299f12c9d6ec02a6

move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative

remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)

remove Metric_Spaces and move its content into Limits and Real_Vector_Spaces

rename RealVector.thy to Real_Vector_Spaces.thy

--HG--
rename : src/HOL/RealVector.thy => src/HOL/Real_Vector_Spaces.thy