diff --git a/docs/iris.sty b/docs/iris.sty
index 51d4ebae4e1a740268817d74a126f72cd2ed5211..136cc677a69699e009957d1125da0616681685dd 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -287,6 +287,8 @@
 % for now, the update modality looks like a pvs without masks.
 \NewDocumentCommand \upd {} {\mathop{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
 
+\NewDocumentCommand\Acc{O{} O{} m m}{\langle #3 \vsE #4  \rangle_{#1}^{#2}}
+
 
 %% Hoare Triples
 \newcommand*{\hoaresizebox}[1]{%
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 1d33f1f1a5e3877214fb224e7456f766c736cb63..997215f1b968dea78740b6d981524769997b9ded 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -513,6 +513,10 @@ For this reason, we also call such accessors \emph{non-atomic}.
 The reasons accessors are useful is that they let us talk about ``opening X'' (\eg ``opening invariants'') without having to care what X is opened around.
 Furthermore, as we construct more sophisticated and more interesting things that can be opened (\eg invariants that can be ``cancelled'', or STSs), accessors become a useful interface that allows us to mix and match different abstractions in arbitrary ways.
 
+For the special case that $\prop = \propC$ and $\propB = \propB'$, we use the following notation that avoids repetition:
+\[ \Acc[\mask_1][\mask_2]\prop{\Ret x. \propB} \eqdef \prop \vs[\mask_1][\mask_2] \Exists\var. \propB * (\propB \vsW[\mask_2][\mask_1] \prop)  \]
+This accessor is ``idempotent'' in the sense that it doesn't actually change the state.  After applying it, we get our $\prop$ back so we end up where we started.
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "iris"