CHANGELOG.

CHANGELOG.md

@@ -37,6 +37,12 @@ lemma.
 * Add instances `big_sepL_flip_mono'`, `big_sepM_flip_mono'`, etc., which are
   wrappers of instances `big_sep*_mono'` for `flip (⊢)` instead of `(⊢)`. (by
   Yusuke Matsushita)
+* Add lemmas `own_forall` and `own_and` to reason about universal quantification
+  (`∀ .. own`) and conjunctions (`own .. ∧ own ..`) of ghost ownership. (by
+  Travis Hance)
+  + These rules are derived from the primitive rule `ownM_forall` (which is
+    proved in the `uPred` model).
+  + Various corollaries for total cmras (which include `ucmra`s) are provided.
 
 **Changes in `heap_lang`:**