Summary
- HOL-Probability: generalize theorems about cumulative distribution function
- HOL-Probability: move stopping time from AFP/Markov_Models
- HOL-Probability: generalize type of essential supremum
The file was modified | src/HOL/Probability/Distribution_Functions.thy (diff) |
The file was added | src/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) |
The file was modified | src/HOL/Probability/Essential_Supremum.thy (diff) |