Changes

Summary

move monotone from Complete_Partial_Order to Orderings
qualified name to fix integrable_cong ambiguity
Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas

Changeset 75464:84e6f9b542e2 by desharna: move monotone from Complete_Partial_Order to Orderings
The file was modified	`src/HOL/Complete_Partial_Order.thy` (diff)
The file was modified	`src/HOL/Orderings.thy` (diff)
Changeset 75463:8e2285baadba by paulson _lp15@cam.ac.uk_: qualified name to fix integrable_cong ambiguity
The file was modified	`src/HOL/Probability/Levy.thy` (diff)
Changeset 75462:7448423e5dba by paulson _lp15@cam.ac.uk_: Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas
The file was modified	`src/HOL/Analysis/Change_Of_Vars.thy` (diff)
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)
The file was modified	`src/HOL/Analysis/Infinite_Sum.thy` (diff)
The file was modified	`src/HOL/Analysis/Interval_Integral.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Integral_Substitution.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Deriv.thy` (diff)
The file was modified	`src/HOL/Library/Landau_Symbols.thy` (diff)
The file was modified	`src/HOL/Probability/Characteristic_Functions.thy` (diff)
The file was modified	`src/HOL/Probability/Sinc_Integral.thy` (diff)
The file was modified	`src/HOL/Topological_Spaces.thy` (diff)