document iAlways

4025554b · Ralf Jung · 24710264 · 4025554b
Commit 4025554b authored Oct 27, 2017 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 5 additions and 0 deletions

ProofMode.md ProofMode.md +5 -0

No files found.
--- 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
 ------------------