Forked from
Iris / Iris
5988 commits behind the upstream repository.
-
Robbert Krebbers authored
This commit introduces the following soundness statements: - Soundness of pure propositions `⌜ φ ⌝%I → φ`. - Soundness of later `(▷ P)%I → P`. The old soundness statement, `(▷^n ⌜ φ ⌝)%I → φ` is now a derived form.
Robbert Krebbers authoredThis commit introduces the following soundness statements: - Soundness of pure propositions `⌜ φ ⌝%I → φ`. - Soundness of later `(▷ P)%I → P`. The old soundness statement, `(▷^n ⌜ φ ⌝)%I → φ` is now a derived form.
