From 4025554b9172e955b56e95291ba8e1bd8884e336 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 27 Oct 2017 13:40:27 +0200
Subject: [PATCH] document iAlways

---
 ProofMode.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/ProofMode.md b/ProofMode.md
index 8bc2bf2dd..0ca7b0b55 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -121,6 +121,11 @@ Modalities
   an instance of the `ElimModal` type class. Instances include: later, except 0,
   basic update and fancy update.
 
+The persistence modality
+------------------------
+
+- `iAlways` is a synonym for `iIntros "!#"`.
+
 The later modality
 ------------------
 
-- 
GitLab