summaryrefslogtreecommitdiff
path: root/lib/isabelle/Hoare.thy
AgeCommit message (Expand)Author
2020-05-13Make Isabelle lemma generation work with grouped regstateThomas Bauereiss
2018-11-30Rename Undefined outcome to ChooseThomas Bauereiss
2018-07-10Add more Isabelle lemmas to libraryThomas Bauereiss
2018-07-09Add some syntactic sugar for IsabelleThomas Bauereiss
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas Bauereiss
2018-06-21Follow Sail2 renaming in Isabelle libraryThomas Bauereiss
2018-05-18Make named theorem collections of state monad more fine-grainedThomas Bauereiss
2018-05-18Add lemmas about monadic Boolean connectivesThomas Bauereiss
2018-04-18Add a simple Hoare logic for sequential reasoning to the libraryThomas Bauereiss