diff --git a/spec/changelog.tex b/spec/changelog.tex
index 05895633b622adb4c81adfe80f9f57d06afb7ffe..49acb415d70a1b0df2eb271aacfad50820e6e085 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -26,6 +26,13 @@ following changes were implemented in this release.
   \item An index that lists all proof rules was added.
 \end{itemize}
 
+Proof rules:
+\begin{itemize}
+  \item The rule \proofRule{implies_simplify} is no longer allowed to
+  perform the simplification $(\varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2
+  ⇒  \varphi_1\lor \varphi_2$.  This is covered by \proofRule{bool_simplify}.
+\end{itemize}
+
 \subsection*{0.2 --- \DTMdisplaydate{2022}{12}{19}{-1}}
 
 This is an intermediate release.  It collects all changes to the original
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index c9c1b4d31ce0b323202918c8f29d9f941d4cc9d6..83130c4b1aa4cd215f344b1ac3efef999a457461 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -1084,7 +1084,6 @@ The possible transformations are:
     \item $ \varphi \rightarrow  \varphi ⇒ \top$
     \item $\neg \varphi \rightarrow  \varphi ⇒  \varphi$
     \item $ \varphi \rightarrow \neg \varphi ⇒ \neg \varphi$
-    \item $( \varphi_1\rightarrow \varphi_2)\rightarrow \varphi_2 ⇒  \varphi_1\lor \varphi_2$
 \end{itemize}
 \end{RuleDescription}