diff --git a/spec/doc.tex b/spec/doc.tex
index c0b26f1f30e559e8b436924d1fdd6316633f10e2..c354011bc533cb59ce9a758f035f2b337cebf048 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -1790,3 +1790,8 @@ standard.\footnote{See \url{https://smt-lib.github.io/theories-FixedSizeBitVecto
 \bibliography{publications}
 \end{document}
 
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 0f1b08d09fa8e7b9e21d7722dd39b9566744df29..a182005bd1e8cc50faccd09ad776374c8c23b6ae 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -1530,6 +1530,21 @@ constants are unfolded during proof printing. Hence, the slightly strange
 form and the reordering of equalities.
 \end{RuleDescription}
 
+\begin{RuleDescription}{bitblast_extract}
+\begin{AletheX}
+$i$. & \ctxsep & $((\_\ \mathrm{extract}\ i\ j)\ x) \simeq (\mathrm{bbterm}\ x_j; \ldots; x_i)$ & (\currule) \\
+\end{AletheX}
+
+Each term $x_i$ corresponds to whether $i$-th bit of $x$ is true or not, which
+will be represented via an application of the operator ``bit\_of'', i.e.,
+$((\_\ bit\_of\ i)\ x)$, which has a Boolean return type.
+%
+The ``bbterm'' operator takes $n$ Booleans and yields a bit-vector of size $n$
+where the least significant bit is is 1 if the $n$-th argument is true, 0
+otherwise, and so on.
+
+\end{RuleDescription}
+
 \clearpage
 \subsection{Index of Rules}
 \label{sec:alethe:rules-index}