Slides/Slides1.thy
author Christian Urban <urbanc@in.tum.de>
Tue, 25 May 2010 00:24:41 +0100
changeset 2299 09bbed4f21d6
child 2300 9fb315392493
permissions -rw-r--r--
added slides

(*<*)
theory Slides1
imports "LaTeXsugar" "Nominal"
begin

notation (latex output)
  set ("_") and
  Cons  ("_::/_" [66,65] 65) 

(*>*)


text_raw {*
  \renewcommand{\slidecaption}{TU Munich, 28.~May 2010}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[t]
  \frametitle{%
  \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
  \\
  \huge Nominal 2\\[-2mm] 
  \large Or, How to Reason Conveniently with\\[-5mm]
  \large General Bindings\\[15mm]
  \end{tabular}}
  \begin{center}
  joint work with {\bf Cezary} and Brian Huffman\\[0mm] 
  \end{center}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>
  \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}
  \mbox{}\\[-3mm]


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}<1>[c]
  \frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}}
  \mbox{}\\[-3mm]

  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}



(*<*)
end
(*>*)