diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 72e333f66f72..389010b828b2 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -495,7 +495,7 @@ macro (name := rwSeq) "rw " c:(config)? s:rwRuleSeq l:(location)? : tactic =>
     `(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))))
   | _ => Macro.throwUnsupported
 
-/-- `rwa` calls `rw`, then closes any remaining goals using `assumption`. -/
+/-- `rwa` is short-hand for `rw; assumption`. -/
 macro "rwa " rws:rwRuleSeq loc:(location)? : tactic =>
   `(tactic| (rw $rws:rwRuleSeq $[$loc:location]?; assumption))