--- /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