Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. clean up prove for inter_interior_unions_intervals
  2. HOL-Multivariate_Analysis: rename theories for more descriptive names
  3. HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
Changeset 63595:aca2659ebba7 by hoelzl:
clean up prove for inter_interior_unions_intervals
The file was modified src/HOL/Multivariate_Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 63594:bd218a9320b5 by hoelzl:
HOL-Multivariate_Analysis: rename theories for more descriptive names
The file was addedsrc/HOL/Multivariate_Analysis/Cauchy_Integral_Theorem.thy
The file was addedsrc/HOL/Multivariate_Analysis/Continuous_Extension.thy
The file was addedsrc/HOL/Multivariate_Analysis/Fashoda_Theorem.thy
The file was addedsrc/HOL/Multivariate_Analysis/Gamma_Function.thy
The file was addedsrc/HOL/Multivariate_Analysis/Henstock_Kurzweil_Integration.thy
The file was addedsrc/HOL/Multivariate_Analysis/Poly_Roots.thy
The file was addedsrc/HOL/Multivariate_Analysis/Summation_Tests.thy
The file was addedsrc/HOL/Multivariate_Analysis/Weierstrass_Theorems.thy
The file was modified src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Integral_Test.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Uniform_Limit.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was removedsrc/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
The file was removedsrc/HOL/Multivariate_Analysis/Extension.thy
The file was removedsrc/HOL/Multivariate_Analysis/Fashoda.thy
The file was removedsrc/HOL/Multivariate_Analysis/Gamma.thy
The file was removedsrc/HOL/Multivariate_Analysis/Integration.thy
The file was removedsrc/HOL/Multivariate_Analysis/PolyRoots.thy
The file was removedsrc/HOL/Multivariate_Analysis/Summation.thy
The file was removedsrc/HOL/Multivariate_Analysis/Weierstrass.thy
Changeset 63593:bbcb05504fdc by hoelzl:
HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
The file was modified src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Extension.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Integration.thy (diff)
The file was modified src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy (diff)