Skip to content
Success

Changes

Summary

  1. Markov_Models: add MDP components; show the existence of a partition into maximal end components
Changeset 7590:1cf167bae3a6 by hoelzl:
Markov_Models: add MDP components; show the existence of a partition into maximal end components
The file was addedthys/Markov_Models/ex/MDP_RP.thy