--- a/Paper/Paper.thy	Tue Feb 08 12:01:28 2011 +0000
+++ b/Paper/Paper.thy	Tue Feb 08 15:50:26 2011 +0000
@@ -327,7 +327,7 @@
 
   \noindent
   It is straightforward to show that @{thm lang_is_union_of_finals} and 
-  @{thm finals_included_in_UNIV} hold. 
+  @{thm finals_in_partitions} hold. 
   Therefore if we know that there exists a regular expression for every
   equivalence class in @{term "finals A"} (which by assumption must be
   a finite set), then we can combine these regular expressions with @{const ALT}
@@ -335,7 +335,7 @@
 
 
   We prove Thm.~\ref{myhillnerodeone} by giving a method that can calculate a
-  regular expression for \emph{every} equivalence classe, not just the ones 
+  regular expression for \emph{every} equivalence class, not just the ones 
   in @{term "finals A"}. We
   first define a notion of \emph{transition} between equivalence classes
   %