Commit c85f2e0d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'master' into 'master'

fix typo in the docs

See merge request iris/iris!310
parents eaeb5851 a0b4ccc2
......@@ -79,7 +79,7 @@ With this lemma in hand, the proof of \thmref{thm:counterexample-1} is simple.
\label{app:section:invariants-without-a-later}
Now we come to the main paradox: if we remove the $\later$ from \ruleref{inv-open}, the logic becomes inconsistent.
The theorem is stated as general as possible so taht it also applies to previous, less powerful versions of Iris.
The theorem is stated as general as possible so that it also applies to previous, less powerful versions of Iris.
\begin{thm}
\label{thm:counterexample-2}
......
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