From eddbdd77b85c44728e0a749fd224d3ce31770976 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 22 Oct 2024 18:02:39 +0200
Subject: [PATCH] doc: refine rwa docstring (#5811)

fixes #5792
---
 src/Init/Tactics.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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))