Slides/Slides1.thy
changeset 2348 09b476c20fe1
parent 2313 25d2cdf7d7e4
child 2740 a9e63abf3feb
equal deleted inserted replaced
2347:9807d30c0e54 2348:09b476c20fe1
    60   \only<1>{
    60   \only<1>{
    61   \begin{textblock}{6}(1.5,11)
    61   \begin{textblock}{6}(1.5,11)
    62   \small
    62   \small
    63   for example\\
    63   for example\\
    64   \begin{tabular}{l@ {\hspace{2mm}}l}
    64   \begin{tabular}{l@ {\hspace{2mm}}l}
    65   \pgfuseshading{smallspherered} & a $\fresh$ Lam [a]. t\\
    65    & a $\fresh$ Lam [a]. t\\
    66   \pgfuseshading{smallspherered} & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\
    66    & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\
    67   \pgfuseshading{smallspherered} & Barendregt-style reasoning about bound variables\\
    67    & Barendregt-style reasoning about bound variables\\
    68   \end{tabular}
    68   \end{tabular}
    69   \end{textblock}}
    69   \end{textblock}}
    70   
    70   
    71   \end{frame}}
    71   \end{frame}}
    72   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
    72   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
   380   \end{itemize}
   380   \end{itemize}
   381 
   381 
   382   \only<1>{
   382   \only<1>{
   383   \begin{textblock}{8}(3,8.5)
   383   \begin{textblock}{8}(3,8.5)
   384   \begin{tabular}{l@ {\hspace{2mm}}p{8cm}}
   384   \begin{tabular}{l@ {\hspace{2mm}}p{8cm}}
   385   \pgfuseshading{smallspherered} & $as$ is a set of names\ldots the binders\\
   385    & $as$ is a set of names\ldots the binders\\
   386   \pgfuseshading{smallspherered} & $x$ is the body (might be a tuple)\\
   386    & $x$ is the body (might be a tuple)\\
   387   \pgfuseshading{smallspherered} & $\approx_{\text{set}}$ is where the cardinality 
   387    & $\approx_{\text{set}}$ is where the cardinality 
   388   of the binders has to be the same\\
   388   of the binders has to be the same\\
   389   \end{tabular}
   389   \end{tabular}
   390   \end{textblock}}
   390   \end{textblock}}
   391 
   391 
   392   \only<4->{
   392   \only<4->{