diff --git a/ProofMode.md b/ProofMode.md
index cc19fdf3d8368ba37d0654b94d7e772a3b5c4726..06ba8e1c82d4bba30dfc53127761313d423e5c16 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -150,11 +150,22 @@ Induction
variables `x1 ... xn`, the hypotheses given by the selection pattern `selpat`,
and the spatial context.
-Rewriting
----------
+Rewriting / simplification
+--------------------------
+
+- `iRewrite pm_trm` / `iRewrite pm_trm in "H"` : rewrite using an internal
+ equality in the proof mode goal / hypothesis `H`.
+- `iEval (tac)` / `iEval (tac) in H` : performs a tactic `tac` on the proof mode
+ goal / hypothesis `H`. The tactic `tac` should be a reduction or rewriting
+ tactic like `simpl`, `cbv`, `lazy`, `rewrite` or `setoid_rewrite`. The `iEval`
+ tactic is implemented by running `tac` on `?evar ⊢ P` / `P ⊢ ?evar` where `P`
+ is the proof goal / hypothesis `H`. After running `tac`, `?evar` is unified
+ with the resulting `P`, which in turn becomes the new proof mode goal /
+ hypothesis `H`.
+ Note that parentheses around `tac` are needed.
+- `iSimpl` / `iSimpl in H` : performs `simpl` on the proof mode goal /
+ hypothesis `H`. This is a shorthand for `iEval (simpl)`.
-- `iRewrite pm_trm` : rewrite an equality in the conclusion.
-- `iRewrite pm_trm in "H"` : rewrite an equality in the hypothesis `H`.
Iris
----