Slides/Slides1.thy
changeset 2348 09b476c20fe1
parent 2313 25d2cdf7d7e4
child 2740 a9e63abf3feb
--- a/Slides/Slides1.thy	Wed Jul 07 13:13:18 2010 +0100
+++ b/Slides/Slides1.thy	Fri Jul 09 10:00:37 2010 +0100
@@ -62,9 +62,9 @@
   \small
   for example\\
   \begin{tabular}{l@ {\hspace{2mm}}l}
-  \pgfuseshading{smallspherered} & a $\fresh$ Lam [a]. t\\
-  \pgfuseshading{smallspherered} & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\
-  \pgfuseshading{smallspherered} & Barendregt-style reasoning about bound variables\\
+   & a $\fresh$ Lam [a]. t\\
+   & Lam [a]. (Var a) \alert{$=$} Lam [b]. (Var b)\\
+   & Barendregt-style reasoning about bound variables\\
   \end{tabular}
   \end{textblock}}
   
@@ -382,9 +382,9 @@
   \only<1>{
   \begin{textblock}{8}(3,8.5)
   \begin{tabular}{l@ {\hspace{2mm}}p{8cm}}
-  \pgfuseshading{smallspherered} & $as$ is a set of names\ldots the binders\\
-  \pgfuseshading{smallspherered} & $x$ is the body (might be a tuple)\\
-  \pgfuseshading{smallspherered} & $\approx_{\text{set}}$ is where the cardinality 
+   & $as$ is a set of names\ldots the binders\\
+   & $x$ is the body (might be a tuple)\\
+   & $\approx_{\text{set}}$ is where the cardinality 
   of the binders has to be the same\\
   \end{tabular}
   \end{textblock}}