From 746dee0935127fce300e7498f20b06ca1c61377b Mon Sep 17 00:00:00 2001
From: lprv <100177227+lprv@users.noreply.github.com>
Date: Tue, 9 Dec 2025 16:41:54 +0000
Subject: [PATCH] [basic.def] Mark definition of "redeclaration" as such

---
 source/basic.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/source/basic.tex b/source/basic.tex
index a78628ca87..447d5deb72 100644
--- a/source/basic.tex
+++ b/source/basic.tex
@@ -177,7 +177,7 @@
 If so, the
 declaration specifies the interpretation and semantic properties of these names.
 A declaration of an entity $X$ is
-a redeclaration of $X$
+a \defn{redeclaration} of $X$
 if another declaration of $X$ is reachable from it\iref{module.reach};
 otherwise, it is a \defnadj{first}{declaration}.