Slides/Slides1.thy
changeset 2299 09bbed4f21d6
child 2300 9fb315392493
--- /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<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
+(*>*)
\ No newline at end of file