Commit 9e72d10e authored by Ralf Jung's avatar Ralf Jung
Browse files


parent 31afcab0
......@@ -88,6 +88,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
`big_sepL_lookup_acc_impl`, `big_sepL2_lookup_acc_impl`,
`big_sepM_lookup_acc_impl`, `big_sepM2_lookup_acc_impl`,
`big_sepS_elem_of_acc_impl`, `big_sepMS_elem_of_acc_impl`.
* Add lemmas `big_sepM_filter'` and `big_sepM_filter` matching the corresponding
`big_sepS` lemmas.
**Changes in `proofmode`:**
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment