summaryrefslogtreecommitdiff
path: root/lib/coq/Sail2_state_monad_lemmas.v
AgeCommit message (Expand)Author
2019-08-22Coq: tactics to do rewrites under state monad, simple wp computationBrian Campbell
2019-08-14Coq library work for proofs:Brian Campbell
2019-07-25Basic port of proof machinery to CoqBrian Campbell