Slides/Slides2.thy
changeset 275 55dc9ff45b73
parent 274 6bf48979a72e
child 276 6f71b016cbe7
equal deleted inserted replaced
274:6bf48979a72e 275:55dc9ff45b73
   595 *}
   595 *}
   596 
   596 
   597 text_raw {*
   597 text_raw {*
   598   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   598   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   599   \mode<presentation>{
   599   \mode<presentation>{
   600   \begin{frame}[t]
   600   \begin{frame}[b]
   601   \frametitle{Undecidability}%
   601   \frametitle{Undecidability}%
   602 
   602 
   603   \begin{center}
   603   \begin{textblock}{7}(4,2.4)
   604   @{thm tcontra_def}
   604   @{thm tcontra_def}
   605   \end{center}
   605   \end{textblock}
   606   
   606   
   607   \only<2>{
   607   \only<2>{
   608   \begin{itemize}
   608   \begin{itemize}
   609   \item Suppose @{text H} decides @{text contra} called with code 
   609   \item Suppose @{text H} decides @{text contra} called with code 
   610   of @{text contra} halts, then\smallskip
   610   of @{text contra} halts, then\smallskip