From abcbcf05cf6e5fce8061fc843a6cbf08b34ac786 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Thu, 8 Aug 2024 10:48:37 -0500
Subject: [PATCH] Rename or_intro to weakening
---
spec/changelog.tex | 2 +-
spec/rule_list.tex | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/spec/changelog.tex b/spec/changelog.tex
index 65f5a42..d5b9489 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 645b87d..26b3b84 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$) \\
--
GitLab