Skip to content
Failed

Changes

Summary

  1. updated generated file;
  2. tuned proofs -- avoid low-level lemmas;
  3. moved lemma to main HOL;
  4. tuned proof;
  5. tuned whitespace;
Changeset 7140:d36bda3d8aea by wenzelm:
updated generated file;
The file was modified thys/Refine_Imperative_HOL/benchmarks/Dijkstra/isabelle/dijkstra_export.sml (diff)
Changeset 7139:fb15c03089f1 by wenzelm:
tuned proofs -- avoid low-level lemmas;
The file was modified thys/Markov_Models/Discrete_Time_Markov_Chain.thy (diff)
The file was modified thys/Probabilistic_Noninterference/Resumption_Based.thy (diff)
Changeset 7138:27ffcc03ef4d by wenzelm:
moved lemma to main HOL;
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)
Changeset 7137:976b25916293 by wenzelm:
tuned proof;
The file was modified thys/LatticeProperties/Conj_Disj.thy (diff)
Changeset 7136:2462ef7dc204 by wenzelm:
tuned whitespace;
The file was modified thys/Multirelations/ROOT (diff)