Commit fd729747 authored by Ralf Jung's avatar Ralf Jung

missed a caption

parent d31256c0
Pipeline #5831 passed with stages
in 9 minutes and 25 seconds
...@@ -212,7 +212,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $ ...@@ -212,7 +212,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
} }
\end{mathparpagebreakable} \end{mathparpagebreakable}
\subsection{Proof rules} \subsection{Proof Rules}
\label{sec:proof-rules} \label{sec:proof-rules}
The judgment $\vctx \mid \prop \proves \propB$ says that with free variables $\vctx$, proposition $\propB$ holds whenever assumption $\prop$ holds. The judgment $\vctx \mid \prop \proves \propB$ says that with free variables $\vctx$, proposition $\propB$ holds whenever assumption $\prop$ holds.
......
Markdown is supported
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