Summary
- Markov_Models: introduce T_coinduct
The file was modified | thys/Markov_Models/Discrete_Time_Markov_Chain.thy (diff) |
The file was modified | thys/Markov_Models/Trace_Space_Equals_Markov_Processes.thy (diff) |
The file was modified | thys/Markov_Models/Discrete_Time_Markov_Chain.thy (diff) |
The file was modified | thys/Markov_Models/Trace_Space_Equals_Markov_Processes.thy (diff) |