diff --git a/RELEASES.md b/RELEASES.md
index a9be10dc99..e893a9c259 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,6 +1,12 @@
 Unreleased
 ---------
 
+* Add tactic macro
+```lean
+macro "stop" s:tacticSeq : tactic => `(repeat sorry)
+```
+See discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Partial.20evaluation.20of.20a.20file).
+
 * When displaying goals, we do not display inaccessible proposition names
 if they do not have forward dependencies. We still display their types.
 For example, the goal
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index a6e6f90671..5b6c964a88 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -443,6 +443,10 @@ syntax (name := split) "split " (colGt term)? (location)? : tactic
 
 syntax (name := dbgTrace) "dbg_trace " str : tactic
 
+/-- Helper tactic for "discarding" the rest of a proof. It is useful when working on the middle of a complex proofs,
+    and less messy than commenting the remainder of the proof. -/
+macro "stop" s:tacticSeq : tactic => `(repeat sorry)
+
 /--
 The tactic `specialize h a₁ ... aₙ` works on local hypothesis `h`.
 The premises of this hypothesis, either universal quantifications or non-dependent implications,