diff --git a/docs/base-logic.tex b/docs/base-logic.tex index 0f7cf136d18eca4451c051bb6421dee38519264f..4daa52d0fcba11b3d83766311dfeaa124245507a 100644 --- a/docs/base-logic.tex +++ b/docs/base-logic.tex @@ -376,18 +376,18 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda \paragraph{Laws for the resource update modality.} \begin{mathpar} -\infer[upd-mono] +\inferH{upd-mono} {\prop \proves \propB} {\upd\prop \proves \upd\propB} -\infer[upd-intro] +\inferH{upd-intro} {}{\prop \proves \upd \prop} -\infer[upd-trans] +\inferH{upd-trans} {} {\upd \upd \prop \proves \upd \prop} -\infer[upd-frame] +\inferH{upd-frame} {}{\propB * \upd\prop \proves \upd (\propB * \prop)} \inferH{upd-update}