Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. HOL-Probability: generalize theorems about cumulative distribution function
  2. HOL-Probability: move stopping time from AFP/Markov_Models
  3. HOL-Probability: generalize type of essential supremum
Changeset 64321:95be866e49fc by hoelzl:
HOL-Probability: generalize theorems about cumulative distribution function
The file was modified src/HOL/Probability/Distribution_Functions.thy (diff)
Changeset 64320:ba194424b895 by hoelzl:
HOL-Probability: move stopping time from AFP/Markov_Models
The file was addedsrc/HOL/Probability/Stopping_Time.thy
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/Measurable.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy (diff)
The file was modified src/HOL/Library/Stream.thy (diff)
The file was modified src/HOL/Probability/Giry_Monad.thy (diff)
The file was modified src/HOL/Probability/Probability.thy (diff)
The file was modified src/HOL/Probability/Stream_Space.thy (diff)
Changeset 64319:a33bbac43359 by hoelzl:
HOL-Probability: generalize type of essential supremum
The file was modified src/HOL/Probability/Essential_Supremum.thy (diff)