Changes

Summary

merged
tuned
reorganized and added log-related lemmas
merged
unscrambling esp of Henstock_lemma_part1
starting to unscramble bounded_variation_absolutely_integrable_interval
tuned proofs
reorganization of tree lemmas; new lemmas

Changeset 66517:7c7977f6c4ce by nipkow: merged
Changeset 66516:97c2d3846e10 by nipkow: tuned
The file was modified	`src/HOL/Data_Structures/Balance.thy` (diff)
Changeset 66515:85c505c98332 by nipkow: reorganized and added log-related lemmas
The file was modified	`src/HOL/Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Archimedean_Field.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Balance.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/MIR.thy` (diff)
The file was modified	`src/HOL/Library/Tree_Real.thy` (diff)
The file was modified	`src/HOL/Real.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
Changeset 66514:70e3f446bfc7 by paulson: merged
Changeset 66513:ca8b18baf0e0 by paulson _lp15@cam.ac.uk_: unscrambling esp of Henstock_lemma_part1
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
Changeset 66512:89b6455b63b6 by paulson _lp15@cam.ac.uk_: starting to unscramble bounded_variation_absolutely_integrable_interval
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Gamma_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
Changeset 66511:9756684f4d74 by nipkow: tuned proofs
The file was modified	`src/HOL/Transcendental.thy` (diff)
Changeset 66510:ca7a369301f6 by nipkow: reorganization of tree lemmas; new lemmas
The file was added	`src/HOL/Library/Tree_Real.thy`
The file was modified	`src/HOL/Data_Structures/Balance.thy` (diff)
The file was modified	`src/HOL/Library/Library.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)