Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Trying out "subgoal", and no more [| |]
  2. HOL-Analysis: fix latex generation
  3. Probability: fix proof
  4. Library: fix name Product_plus to Product_Plus
  5. HOL-Analysis: move Product_Vector and Inner_Product from Library
  6. HOL-Analysis: move Continuum_Not_Denumerable from Library
  7. HOL-Analysis: move Library/Convex to Convex_Euclidean_Space
  8. 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)
  9. new material on paths, etc. Also rationalisation
  10. Merged
  11. Set_Permutations replaced by more general Multiset_Permutations
Changeset 63975:6728b5007ad0 by paulson _lp15@cam.ac.uk_:
Trying out "subgoal", and no more [| |]
The file was modified src/HOL/Auth/OtwayRees.thy (diff)
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)
Changeset 63967:2aa42596edc3 by paulson _lp15@cam.ac.uk_:
new material on paths, etc. Also rationalisation
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Filter.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
Changeset 63966:957ba35d1338 by manuel eberl _eberlm@in.tum.de_:
Merged
Changeset 63965:d510b816ea41 by eberlm _eberlm@in.tum.de_:
Set_Permutations replaced by more general Multiset_Permutations
The file was addedsrc/HOL/Library/Multiset_Permutations.thy
The file was modified src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Probability/Random_Permutations.thy (diff)
The file was removedsrc/HOL/Library/Set_Permutations.thy