Summary
- updated generated file;
- tuned proofs -- avoid low-level lemmas;
- moved lemma to main HOL;
- tuned proof;
- tuned whitespace;
The file was modified | thys/Refine_Imperative_HOL/benchmarks/Dijkstra/isabelle/dijkstra_export.sml (diff) |
The file was modified | thys/Markov_Models/Discrete_Time_Markov_Chain.thy (diff) |
The file was modified | thys/Probabilistic_Noninterference/Resumption_Based.thy (diff) |
The file was modified | thys/Multirelations/C_Algebras.thy (diff) |
The file was modified | thys/Multirelations/Multirelations.thy (diff) |
The file was modified | thys/Refine_Monadic/Refine_Misc.thy (diff) |
The file was modified | thys/LatticeProperties/Conj_Disj.thy (diff) |
The file was modified | thys/Multirelations/ROOT (diff) |