# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1374616733 -7200
# Node ID c6aa1be1033a449c7ea7572d390c281499a03629
# Parent  6f71b016cbe7437cc810dd4d7bb5ecb226dbcdbc
slides

diff -r 6f71b016cbe7 -r c6aa1be1033a Slides/Slides2.thy
--- 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}
   
 
diff -r 6f71b016cbe7 -r c6aa1be1033a slides2.pdf
Binary file slides2.pdf has changed