diff --git a/spec/changelog.tex b/spec/changelog.tex
index 65f5a4246502de886804b5ccbc8195134876e7a9..d5b94898c35cff05348b066132177dddfef8ba87 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -11,7 +11,7 @@ Proof rules:
   of equality explicitly but as an equivalence. Note that in principle this
   could be done with the rule \proofRule{symm} above, but would require a long
   and tedious use of \proofRule{subproof} for each direction of the equivalence.
-  \item Addition of the rule \proofRule{or_intro} to express weakening of a
+  \item Addition of the rule \proofRule{weakening} to express weakening of a
         clause.
 \end{itemize}
 
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 645b87dca9ef2637b7d9b9b00545a38f871d99ae..26b3b8499ef1ff51778e2d37a90bcd8a3798f209 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -263,7 +263,7 @@ simplifications.}
 \label{rule-tab:cvc5}\\
   Rule & Description \\
   \hline
-\ruleref{or_intro} & Weakening of a clause. \\
+\ruleref{weakening} & Weakening of a clause. \\
 \ruleref{eq_symmetric} & Symmetry of equality as equivalence. \\
 \end{xltabular}
 \subsection{Rule List}
@@ -845,7 +845,7 @@ An application of the \proofRule{or} rule.
 \end{AletheVerb}
 \end{RuleExample}
 
-\begin{RuleDescription}{or_intro}
+\begin{RuleDescription}{weakening}
 \begin{AletheX}
 $i$. & \ctxsep &
 $\varphi_1, \cdots, \varphi_n$ & ($\dots$) \\