--- a/Paper/Paper.thy	Tue Mar 15 15:53:22 2011 +0000
+++ b/Paper/Paper.thy	Wed Mar 23 12:17:30 2011 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Myhill" "LaTeXsugar" 
+imports "../Myhill_2" "~~/src/HOL/Library/LaTeXsugar" 
 begin
 
 declare [[show_question_marks = false]]
@@ -878,7 +878,7 @@
 
   \begin{proof}[Base Cases]
   The cases for @{const NULL}, @{const EMPTY} and @{const CHAR} are routine, because 
-  we can easily establish
+  we can easily establish that
 
   \begin{center}
   \begin{tabular}{l}
@@ -937,7 +937,7 @@
   finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"},
   and so also finite. Injectivity amounts to showing that @{text "X = Y"} under the
   assumptions that @{text "X, Y \<in> "}~@{term "UNIV // =tag="} and @{text "f X = f Y"}.
-  From the assumption we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with 
+  From the assumptions we can obtain @{text "x \<in> X"} and @{text "y \<in> Y"} with 
   @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in 
   turn means that the equivalence classes @{text X}
   and @{text Y} must be equal.\qed
@@ -1318,7 +1318,7 @@
 
 
   Our formalisation consists of 780 lines of Isabelle/Isar code for the first
-  direction and 475 for the second, plus around 300 lines of standard material about
+  direction and 460 for the second, plus around 300 lines of standard material about
   regular languages. While this might be seen as too large to count as a
   concise proof pearl, this should be seen in the context of the work done by
   Constable at al \cite{Constable00} who formalised the Myhill-Nerode theorem