Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Markov_Models: add AE_T_ev_HLD_infinite
  2. Markov_Models: transfer measures along a relation induced by a function
  3. Markov_Models: generalized coinduction rule for stream measures
Changeset 8741:31b41e185ea8 by hoelzl:
Markov_Models: add AE_T_ev_HLD_infinite
The file was modified thys/Markov_Models/Discrete_Time_Markov_Chain.thy (diff)
Changeset 8740:a34494f74c66 by hoelzl:
Markov_Models: transfer measures along a relation induced by a function
The file was modified thys/Markov_Models/Discrete_Time_Markov_Chain.thy (diff)
Changeset 8739:f79d3fdbcf50 by hoelzl:
Markov_Models: generalized coinduction rule for stream measures
The file was modified thys/Markov_Models/Discrete_Time_Markov_Chain.thy (diff)
The file was modified thys/Markov_Models/Markov_Decision_Process.thy (diff)