Skip to content
Snippets Groups Projects
Commit 186412a7 authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

Apply 1 suggestion(s) to 1 file(s)

parent 5eff5bfd
No related branches found
No related tags found
1 merge request!306Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼`
Pipeline #51143 passed
......@@ -128,7 +128,7 @@ API-breaking change is listed.
- Add `union_subseteq_l'`, `union_subseteq_r'` as transitive versions of
`union_subseteq_l`, `union_subseteq_r` that can be more easily `apply`ed.
- Rename `gmultiset_elem_of_singleton_subseteq``gmultiset_singleton_subseteq_l`
and swap the order to be consistent with Iris's `singleton_included_l`. Add
and swap the equivalence to be consistent with Iris's `singleton_included_l`. Add
`gmultiset_singleton_subseteq`, which is similar to `singleton_included` in
Iris.
- Add lemmas `singleton_subseteq_l` and `singleton_subseteq` for sets.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment