Changes

Summary

de-applying and meta-quantifying
merged
more renaming fixes
fixes and more de-applying
more de-applying and a fix
merged
last bit of renaming
de-applying
Added Real_Asymp package
Tagged Conformal_Mappings in HOL-Analysis

Changeset 68638:87d1bff264df by paulson _lp15@cam.ac.uk_: de-applying and meta-quantifying
The file was modified	`src/HOL/Analysis/Interval_Integral.thy` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
Changeset 68637:ec8c7c9459e0 by paulson: merged
Changeset 68636:f33ffa0a27a1 by paulson _lp15@cam.ac.uk_: more renaming fixes
The file was modified	`src/Doc/Tutorial/Types/Numbers.thy` (diff)
Changeset 68635:8094b853a92f by paulson _lp15@cam.ac.uk_: fixes and more de-applying
The file was modified	`src/Doc/Tutorial/Types/Numbers.thy` (diff)
The file was modified	`src/Doc/Tutorial/document/numerics.tex` (diff)
The file was modified	`src/HOL/Analysis/Borel_Space.thy` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
Changeset 68634:db0980691ef4 by paulson _lp15@cam.ac.uk_: more de-applying and a fix
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Further_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Riemann_Mapping.thy` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Quadratic_Reciprocity.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
The file was modified	`src/HOL/ex/Gauge_Integration.thy` (diff)
Changeset 68633:ae4373f3d8d3 by paulson: merged
Changeset 68632:98014d34847e by paulson _lp15@cam.ac.uk_: last bit of renaming
The file was modified	`src/HOL/Decision_Procs/cooper_tac.ML` (diff)
The file was modified	`src/HOL/Tools/Qelim/cooper.ML` (diff)
Changeset 68631:bc1369804692 by paulson _lp15@cam.ac.uk_: de-applying
The file was modified	`src/HOL/Divides.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Quadratic_Reciprocity.thy` (diff)
Changeset 68630:c55f6f0b3854 by manuel eberl _eberlm@in.tum.de_: Added Real_Asymp package
The file was added	`src/Doc/Real_Asymp/Real_Asymp_Doc.thy`
The file was added	`src/Doc/Real_Asymp/document/root.tex`
The file was added	`src/Doc/Real_Asymp/document/style.sty`
The file was added	`src/HOL/Real_Asymp/Eventuallize.thy`
The file was added	`src/HOL/Real_Asymp/Inst_Existentials.thy`
The file was added	`src/HOL/Real_Asymp/Lazy_Eval.thy`
The file was added	`src/HOL/Real_Asymp/Multiseries_Expansion.thy`
The file was added	`src/HOL/Real_Asymp/Multiseries_Expansion_Bounds.thy`
The file was added	`src/HOL/Real_Asymp/Real_Asymp.thy`
The file was added	`src/HOL/Real_Asymp/Real_Asymp_Approx.thy`
The file was added	`src/HOL/Real_Asymp/Real_Asymp_Examples.thy`
The file was added	`src/HOL/Real_Asymp/asymptotic_basis.ML`
The file was added	`src/HOL/Real_Asymp/exp_log_expression.ML`
The file was added	`src/HOL/Real_Asymp/expansion_interface.ML`
The file was added	`src/HOL/Real_Asymp/inst_existentials.ML`
The file was added	`src/HOL/Real_Asymp/lazy_eval.ML`
The file was added	`src/HOL/Real_Asymp/multiseries_expansion.ML`
The file was added	`src/HOL/Real_Asymp/multiseries_expansion_bounds.ML`
The file was added	`src/HOL/Real_Asymp/real_asymp.ML`
The file was added	`src/HOL/Real_Asymp/real_asymp_diag.ML`
The file was modified	`CONTRIBUTORS` (diff)
The file was modified	`NEWS` (diff)
The file was modified	`src/Doc/ROOT` (diff)
The file was modified	`src/HOL/ROOT` (diff)
Changeset 68629:f36858fdf768 by wenda li _wl302@cam.ac.uk_: Tagged Conformal_Mappings in HOL-Analysis
The file was modified	`src/HOL/Analysis/Conformal_Mappings.thy` (diff)