Add more text

1 files changed, 1 insertions, 1 deletions

diff --git a/main.tex b/main.tex
index cf618c0..f5768b3 100644
--- a/main.tex
+++ b/main.tex
@@ -184,7 +184,7 @@ The solution to both of these points is to have a formally verified high-level s
 
 \paragraph{How could such a tool be constructed?}
 
-The radical solution to this problem is to formally verify the complete tool, writing the complete tool in Coq~\cite{coquand86}
+The radical solution to this problem is to formally verify the complete tool, writing the complete tool in Coq~\cite{coquand86}, an interactive theorem prover.
 
 \section{Guarantees of trusted code}