Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. HOL-Analysis: fix latex generation
  2. Probability: fix proof
  3. Library: fix name Product_plus to Product_Plus
  4. HOL-Analysis: move Product_Vector and Inner_Product from Library
  5. HOL-Analysis: move Continuum_Not_Denumerable from Library
  6. HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
  7. HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
Changeset 63974:721810140424 by hoelzl:
HOL-Analysis: fix latex generation
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
Changeset 63973:b09f16aeb694 by hoelzl:
Probability: fix proof
The file was modified src/HOL/Probability/Probability_Mass_Function.thy (diff)
Changeset 63972:c98d1dd7eba1 by hoelzl:
Library: fix name Product_plus to Product_Plus
The file was addedsrc/HOL/Library/Product_Plus.thy
The file was modified src/HOL/Analysis/Product_Vector.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Library/Product_Order.thy (diff)
The file was removedsrc/HOL/Library/Product_plus.thy
Changeset 63971:da89140186e2 by hoelzl:
HOL-Analysis: move Product_Vector and Inner_Product from Library
The file was addedsrc/HOL/Analysis/Inner_Product.thy
The file was addedsrc/HOL/Analysis/Product_Vector.thy
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Mirabelle/ex/Ex.thy (diff)
The file was removedsrc/HOL/Library/Inner_Product.thy
The file was removedsrc/HOL/Library/Product_Vector.thy
Changeset 63970:3b6a3632e754 by hoelzl:
HOL-Analysis: move Continuum_Not_Denumerable from Library
The file was addedsrc/HOL/Analysis/Continuum_Not_Denumerable.thy
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Hahn_Banach/Bounds.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Probability/Distribution_Functions.thy (diff)
The file was modified src/HOL/Probability/ex/Measure_Not_CCC.thy (diff)
The file was removedsrc/HOL/Library/Continuum_Not_Denumerable.thy
Changeset 63969:f4b4fba60b1d by hoelzl:
HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was removedsrc/HOL/Library/Convex.thy
Changeset 63968:4359400adfe7 by hoelzl:
HOL-Analysis: the image of a negligible set under a Lipschitz continuous function is negligible (based on HOL Light proof ported by L. C. Paulson)
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/Complete_Measure.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)