# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1374585252 -7200
# Node ID 6bf48979a72e59fc63b9faf634c7ea702458d4bd
# Parent  fa021a0c698437d8c336e6bc6c4cee27beb27acc
new version

diff -r fa021a0c6984 -r 6bf48979a72e Slides/Slides2.thy
--- a/Slides/Slides2.thy	Tue Jul 23 14:52:22 2013 +0200
+++ b/Slides/Slides2.thy	Tue Jul 23 15:14:12 2013 +0200
@@ -261,6 +261,12 @@
   \end{tikzpicture}
   \end{textblock}}
 
+  \only<4->{
+  \begin{textblock}{4}(4.2,12.4)
+  \begin{tikzpicture}
+  \draw (0,0) node {\begin{tabular}{l}correct UTM by translation\end{tabular}};
+  \end{tikzpicture}
+  \end{textblock}}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -704,10 +710,29 @@
 
   \begin{itemize}
   \item feels awfully like reasoning about machine code
-  \item compositional constructions / reasoning
+  \item compositional constructions / reasoning not frictionless
   \item sizes
-  
+
+  \begin{center}
+  \begin{tabular}{ll}
+  & sizes:\smallskip\\
+  UF       & 140843 constructors\\
+  Reg.~Mach.~ & @{text 2} Mio instructions\\
+  UTM      & @{text 38} Mio states\\
+  \end{tabular}
+  \end{center}\pause
+
+  \item an observation: our treatment of recursive functions is a mini-version
+  of the work by\\ Myreen \& Owens about deeply embedding HOL
   \end{itemize}
+ 
+  \only<1>{
+  \begin{textblock}{4}(2,13.9)
+  \begin{tikzpicture}
+  \draw (0,0) node {\small\begin{tabular}{l}$^\star$old version: 
+  RM (@{text 12} Mio) UTM (@{text 112} Mio)\end{tabular}};
+  \end{tikzpicture}
+  \end{textblock}}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -718,44 +743,6 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{Recursive Functions}%
-
-  \begin{itemize}
-  \item addition, multiplication, \ldots
-  \item logical operations, quantifiers\ldots
-  \item coding of numbers (Cantor encoding)
-  \item UF\pause\bigskip
-
-  \item Recursive Functions $\Rightarrow$ Register Machines
-  \item Register Machines $\Rightarrow$ Turing Machines
-  \end{itemize}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{Sizes}%
-
-  \begin{itemize}
-  \item UF (size: @{text 140843})
-  \item Register Machine (size: @{text 2} Mio instructions)
-  \item UTM (size: @{text 38} Mio states)
-  \end{itemize}\bigskip\bigskip
-
-  \small
-  old version: RM (@{text 12} Mio) UTM (@{text 112} Mio)
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
   \frametitle{Separation Algebra}%
 
   \begin{itemize}
diff -r fa021a0c6984 -r 6bf48979a72e slides2.pdf
Binary file slides2.pdf has changed