|
2299
|
1 |
(*<*)
|
|
|
2 |
theory Slides1
|
|
|
3 |
imports "LaTeXsugar" "Nominal"
|
|
|
4 |
begin
|
|
|
5 |
|
|
|
6 |
notation (latex output)
|
|
|
7 |
set ("_") and
|
|
|
8 |
Cons ("_::/_" [66,65] 65)
|
|
|
9 |
|
|
|
10 |
(*>*)
|
|
|
11 |
|
|
|
12 |
|
|
|
13 |
text_raw {*
|
|
|
14 |
\renewcommand{\slidecaption}{TU Munich, 28.~May 2010}
|
|
|
15 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
16 |
\mode<presentation>{
|
|
|
17 |
\begin{frame}<1>[t]
|
|
|
18 |
\frametitle{%
|
|
|
19 |
\begin{tabular}{@ {\hspace{-3mm}}c@ {}}
|
|
|
20 |
\\
|
|
|
21 |
\huge Nominal 2\\[-2mm]
|
|
|
22 |
\large Or, How to Reason Conveniently with\\[-5mm]
|
|
|
23 |
\large General Bindings\\[15mm]
|
|
|
24 |
\end{tabular}}
|
|
|
25 |
\begin{center}
|
|
|
26 |
joint work with {\bf Cezary} and Brian Huffman\\[0mm]
|
|
|
27 |
\end{center}
|
|
|
28 |
\end{frame}}
|
|
|
29 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
30 |
|
|
|
31 |
*}
|
|
|
32 |
|
|
|
33 |
text_raw {*
|
|
|
34 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
35 |
\mode<presentation>{
|
|
|
36 |
\begin{frame}<1>
|
|
|
37 |
\frametitle{\begin{tabular}{c}Part I: Nominal Theory\end{tabular}}
|
|
|
38 |
\mbox{}\\[-3mm]
|
|
|
39 |
|
|
|
40 |
|
|
|
41 |
\end{frame}}
|
|
|
42 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
43 |
*}
|
|
|
44 |
|
|
|
45 |
text_raw {*
|
|
|
46 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
47 |
\mode<presentation>{
|
|
|
48 |
\begin{frame}<1>[c]
|
|
|
49 |
\frametitle{\begin{tabular}{c}Part II: General Bindings\end{tabular}}
|
|
|
50 |
\mbox{}\\[-3mm]
|
|
|
51 |
|
|
|
52 |
|
|
|
53 |
\end{frame}}
|
|
|
54 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
55 |
*}
|
|
|
56 |
|
|
|
57 |
|
|
|
58 |
|
|
|
59 |
(*<*)
|
|
|
60 |
end
|
|
|
61 |
(*>*) |