diff --git a/docs/program-logic.tex b/docs/program-logic.tex index d0dc60bc11674127a3fbbab21eec5c5fc19baef1..d6d711649ccb1b43799f4116b2adaff5527cc578 100644 --- a/docs/program-logic.tex +++ b/docs/program-logic.tex @@ -465,7 +465,6 @@ 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. -\ralf{This would be much more convincing if we had forward references here to sections describing canellable invariants and STSs.} %%% Local Variables: %%% mode: latex