diff --git a/docs/Cryptol.pdf b/docs/Cryptol.pdf
index cfe81c47..f7b324b2 100644
Binary files a/docs/Cryptol.pdf and b/docs/Cryptol.pdf differ
diff --git a/docs/ProgrammingCryptol.pdf b/docs/ProgrammingCryptol.pdf
index cfe81c47..f7b324b2 100644
Binary files a/docs/ProgrammingCryptol.pdf and b/docs/ProgrammingCryptol.pdf differ
diff --git a/docs/ProgrammingCryptol/aes/AES.tex b/docs/ProgrammingCryptol/aes/AES.tex
index 484cd68f..9ebc8497 100644
--- a/docs/ProgrammingCryptol/aes/AES.tex
+++ b/docs/ProgrammingCryptol/aes/AES.tex
@@ -699,7 +699,7 @@ such that {\tt gf28DotProduct} returns the dot-product of two length $n$ vectors
   addition:
 \begin{eqnarray*}
 a \cdot b &=& b \cdot a \\
-a \cdot (b + c) &=& a\cdot b + a\cdot b
+a \cdot (b + c) &=& a\cdot b + a\cdot c
 \end{eqnarray*}
 Addition over vectors is defined element-wise. Prove the commutativity
 property for vectors of length 10.  Distributivity will take much