diff -r aead2aad845c -r 09bbed4f21d6 Slides/Slides1.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Slides/Slides1.thy Tue May 25 00:24:41 2010 +0100 @@ -0,0 +1,61 @@ +(*<*) +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{ + \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{ + \begin{frame}<1> + \frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}} + \mbox{}\\[-3mm] + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + +text_raw {* + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + \mode{ + \begin{frame}<1>[c] + \frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}} + \mbox{}\\[-3mm] + + + \end{frame}} + %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +*} + + + +(*<*) +end +(*>*) \ No newline at end of file