diff -r f631a59ee7af -r 5709254e004f Slides/Slides1.thy
--- a/Slides/Slides1.thy	Wed Aug 24 22:21:37 2011 +0000
+++ b/Slides/Slides1.thy	Thu Aug 25 06:18:58 2011 +0000
@@ -23,7 +23,7 @@
   \begin{tabular}{@ {}c@ {}}
   \Large A Formalisation of the\\[-4mm] 
   \Large Myhill-Nerode Theorem based on\\[-4mm] 
-  \Large Regular Expressions\\[-4mm]
+  \Large \alert<2>{Regular Expressions}\\[-4mm]
   \Large (Proof Pearl)\\[0mm] 
   \end{tabular}}
   
@@ -56,10 +56,10 @@
   \begin{frame}[c]
   \frametitle{}
 
-  \begin{textblock}{12.9}(1.5,3.2)
+  \begin{textblock}{12.9}(1.5,2.0)
   \begin{block}{}
   \begin{minipage}{12.4cm}\raggedright
-  \large I want to teach \alert{students} with
+  \large {\bf Motivation:}\\[2mm]I want to teach \alert{students} with
   theorem\\ provers (especially for inductions).
   \end{minipage}
   \end{block}
@@ -215,9 +215,9 @@
   \end{textblock}}
   \medskip
 
-  \only<6->{A solution:\;\;use \smath{\text{nat}} \;@{text "\<Rightarrow>"}\; state nodes\medskip}
+  \only<6->{\underline{A solution}:\;\;use \smath{\text{nat}} \;@{text "\<Rightarrow>"}\; state nodes\medskip}
 
-  \only<7->{You have to \alert{\underline{rename}} states!}
+  \only<7->{You have to \alert{rename} states!}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -235,7 +235,7 @@
   \end{center}
 
   \begin{itemize}
-  \item Kozen's paper proof of Myhill-Nerode:\\ 
+  \item Kozen's ``paper'' proof of Myhill-Nerode:\\ 
   \hspace{2cm}requires absence of \alert{inaccessible states}
   \end{itemize}\bigskip\bigskip
 
@@ -292,9 +292,7 @@
 
   \begin{itemize}
   \item provides necessary and suf\!ficient conditions\\ for a language 
-  being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\medskip
-
-  \item will help with closure properties of regular languages\bigskip\pause
+  being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\bigskip
 
   \item key is the equivalence relation:\smallskip
   \begin{center}
@@ -340,11 +338,11 @@
   \end{textblock}
 
   \only<2->{%
-  \begin{textblock}{5}(9.4,7.2)
+  \begin{textblock}{5}(9.1,7.2)
   \begin{tikzpicture}
   \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]
   {@{text "\<lbrakk>x\<rbrakk>"}$_{\approx_{A}}$};
-  \draw (0.9,-1.1) node {\begin{tabular}{l}equivalence class\end{tabular}};
+  \draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}};
   \end{tikzpicture}
   \end{textblock}}
 
@@ -708,9 +706,9 @@
 
 
   \item \alt<1>{\smath{\text{pders x r \mbox{$=$} pders y r}}}
-            {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R_1}}} 
+            {\smath{\underbrace{\text{pders x r \mbox{$=$} pders y r}}_{R}}} 
         refines \textcolor{blue}{x $\approx_{{\cal L}(\text{r})}$ y}\\[16mm]\pause
-  \item \smath{\text{finite} (U\!N\!IV /\!/ R_1)} \bigskip\pause
+  \item \smath{\text{finite} (U\!N\!IV /\!/ R)} \bigskip\pause
   \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed.
   \end{itemize}
   
@@ -760,7 +758,7 @@
   \end{block}
   \end{minipage}\medskip\pause
 
-  \small(\smath{A \dn \bigcup_n a^n})
+  \small(\smath{B \dn \bigcup_n a^n})
   \end{quote}
 
   \end{itemize}