Commit c3585db7 authored by Ralf Jung's avatar Ralf Jung
Browse files

docs: typo

parent c83e64a1
...@@ -16,7 +16,7 @@ Now we define: ...@@ -16,7 +16,7 @@ Now we define:
\CInv{\gname}{\namesp}{\prop} \eqdef{}& \knowInv\namesp{\prop \lor \ownGhost\gname{1}} \CInv{\gname}{\namesp}{\prop} \eqdef{}& \knowInv\namesp{\prop \lor \ownGhost\gname{1}}
\end{align*} \end{align*}
It is then straight-forward to prove: It is then straight forward to prove:
\begin{mathpar} \begin{mathpar}
\inferH{CInv-new}{} \inferH{CInv-new}{}
{\later\prop \vs[\bot] \Exists \gname. \CInvTok\gname{1} * \always\CInv\gname\namesp\prop} {\later\prop \vs[\bot] \Exists \gname. \CInvTok\gname{1} * \always\CInv\gname\namesp\prop}
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