# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1374675903 -7200
# Node ID 19a4ac992823bd9bd37d1a62b52ddb107da1f48c
# Parent  98b3b769ec9aba010f65f0d516135925063e3113
slides

diff -r 98b3b769ec9a -r 19a4ac992823 Slides/Slides2.thy
--- a/Slides/Slides2.thy	Wed Jul 24 09:22:05 2013 +0200
+++ b/Slides/Slides2.thy	Wed Jul 24 16:25:03 2013 +0200
@@ -609,7 +609,7 @@
   
   \only<2>{
   \begin{itemize}
-  \item Suppose @{text H} decides @{text contra} called with code 
+  \item Suppose @{text H} decides @{text contra} called with the code 
   of @{text contra} halts, then\smallskip
 
   \begin{center}\small
@@ -634,7 +634,7 @@
   \end{itemize}}
   \only<3>{
   \begin{itemize}
-  \item Suppose @{text H} decides @{text contra} called with code 
+  \item Suppose @{text H} decides @{text contra} called with the code 
   of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{}
 
   \begin{center}\small
@@ -719,7 +719,7 @@
   \begin{center}
   \begin{tabular}{ll}
   & sizes:\smallskip\\
-  UF       & 140843 constructors\\
+  UF       & @{text 140843} constructors\\
   URM      & @{text 2} Mio instructions\\
   UTM      & @{text 38} Mio states\\
   \end{tabular}
@@ -891,7 +891,7 @@
   @{text "\<lbrace>p\<rbrace> c \<lbrace>q\<rbrace>"} @{text "\<equiv>"}\smallskip\\
   & @{text "\<forall> cf r."}\\
   & \hspace{3mm} @{text "(p \<star> c \<star> r) cf"} implies\\
-  & \hspace{3mm} @{text "\<exists> k. "} @{text "(q \<star> c \<star> r) (run k cf)"} 
+  & \hspace{3mm} @{text "\<exists> k. "} @{text "(q \<star> c \<star> r) (steps k cf)"} 
   \end{tabular}
   \end{center}\bigskip\bigskip
 
diff -r 98b3b769ec9a -r 19a4ac992823 slides2.pdf
Binary file slides2.pdf has changed