Slides/Slides2.thy
changeset 278 acc752cef1e7
parent 277 c6aa1be1033a
child 279 98b3b769ec9a
equal deleted inserted replaced
277:c6aa1be1033a 278:acc752cef1e7
   346   \end{tabular}
   346   \end{tabular}
   347   \end{center}
   347   \end{center}
   348   \end{itemize}
   348   \end{itemize}
   349 
   349 
   350   \only<2->{
   350   \only<2->{
   351   \begin{textblock}{4}(0.3,4.2)
   351   \begin{textblock}{4}(0.3,11.8)
   352   \begin{tikzpicture}
   352   \begin{tikzpicture}
   353   \node[ellipse callout, fill=red] at (0, 0){\textcolor{yellow}{Spaghetti Code!}};
   353   \node[ellipse callout, fill=red, callout absolute pointer={(-0.2,1)}] 
       
   354    at (0, 0){\large\fontspec{Chalkduster}\textcolor{yellow}{Spaghetti Code!}};
   354   \end{tikzpicture}
   355   \end{tikzpicture}
   355   \end{textblock}}
   356   \end{textblock}}
   356 
   357 
   357   \end{frame}}
   358   \end{frame}}
   358   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   359   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   740 
   741 
   741 text_raw {*
   742 text_raw {*
   742   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   743   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   743   \mode<presentation>{
   744   \mode<presentation>{
   744   \begin{frame}[c]
   745   \begin{frame}[c]
   745   \frametitle{\begin{tabular}{@ {}c@ {}}Stealing From Other Works\end{tabular}}%
   746   \frametitle{\begin{tabular}{@ {}c@ {}}\Large Inspiration from other Works\end{tabular}}%
   746 
   747 
       
   748   \onslide<3->{
   747   \begin{itemize}
   749   \begin{itemize}
   748   \item Jensen, Benton, Kennedy ({\bf 2013}),
   750   \item Jensen, Benton, Kennedy ({\bf 2013}),
   749   {\it High-Level Separation Logic for Low-Level Code}\medskip\\
   751   {\it High-Level Separation Logic for Low-Level Code}\medskip\\
   750   
   752   
   751   \item Myreen ({\bf 2008}), {\it Formal Verification of Machine-Code Programs},
   753   \item Myreen ({\bf 2008}), {\it Formal Verification of Machine-Code Programs},
   752   PhD thesis\medskip
   754   PhD thesis\medskip
   753 
   755 
   754   \item Klein, Kolanski, Boyton ({\bf 2012}), {\it Mechanised Separation Algebra}
   756   \item Klein, Kolanski, Boyton ({\bf 2012}), {\it Mechanised Separation Algebra}
   755 
   757 
   756   \end{itemize}
   758   \end{itemize}}
       
   759 
       
   760   \only<2->{
       
   761   \begin{textblock}{4}(1.4,0.9)
       
   762   \begin{tikzpicture}
       
   763   \draw (0,0) node {\fontspec{Chalkduster}\textcolor{red!80}{\LARGE Stealing}};
       
   764   \end{tikzpicture}
       
   765   \end{textblock}}
   757   \end{frame}}
   766   \end{frame}}
   758   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   767   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   759 *}
   768 *}
   760 
   769 
   761 text_raw {*
   770 text_raw {*