--- a/Slides/Slides2.thy	Tue Jul 23 23:46:08 2013 +0200
+++ b/Slides/Slides2.thy	Tue Jul 23 23:58:53 2013 +0200
@@ -257,7 +257,7 @@
 
   \begin{textblock}{3}(1,10.0)
   \begin{tikzpicture}
-  \draw (0,0) node {\small\begin{tabular}{l}undecidabilty\\of the halting\\ problem\end{tabular}};
+  \draw (0,0) node {\small\begin{tabular}{l}undecidability\\of the halting\\ problem\end{tabular}};
   \end{tikzpicture}
   \end{textblock}}
 
@@ -313,7 +313,7 @@
   \item @{text steps} function:
 
   \begin{quote}\rm
-  What does the TM claclulate after it has executed @{text n} steps?
+  What does the TM calculate after it has executed @{text n} steps?
   \end{quote}\pause
 
   \item designate the @{text 0}-state as "halting state" and remain there 
@@ -929,7 +929,8 @@
   (ca.~@{text 7000} is the soa \raisebox{-1mm}{\includegraphics[scale=0.077]{smiley.jpg}})
   \bigskip
   
-  \item We learned a lot about current verification technology for low-level code.
+  \item We learned a lot about current verification technology for low-level code
+  (we had no infrastructure: CPU model).
   \end{itemize}