--- a/Myhill_1.thy	Fri Feb 11 12:13:35 2011 +0000
+++ b/Myhill_1.thy	Fri Feb 11 13:30:37 2011 +0000
@@ -499,6 +499,8 @@
 where
   "solve X ES = (if (card ES = 1) then ES else solve X (Iter X ES))"
 
+thm solve.simps
+
 
 text {*
   Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"},

--- a/Paper/Paper.thy	Fri Feb 11 12:13:35 2011 +0000
+++ b/Paper/Paper.thy	Fri Feb 11 13:30:37 2011 +0000
@@ -154,7 +154,7 @@
   \it%
   \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
   `` & If the reader finds the above treatment in terms of bit lists revoltingly
-       concrete, I cannot disagree.''\\
+       concrete, I cannot disagree. A more abstract approach is clearly desirable.''\\
   `` & All lemmas appear obvious given a picture of the composition of automata\ldots
        Yet their proofs require a painful amount of detail.''
   \end{tabular}
@@ -391,7 +391,7 @@
   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 use @{text "\<bigplus>"} to obtain a regular expression 
-  using that matches every string in @{text A}.
+  that matches every string in @{text A}.
 
 
   Our proof of Thm.~\ref{myhillnerodeone} relies on a method that can calculate a
@@ -408,7 +408,7 @@
   which means that if we concatenate the character @{text c} to the end of all 
   strings in the equivalence class @{text Y}, we obtain a subset of 
   @{text X}. Note that we do not define an automaton here, we merely relate two sets
-  (with the help of a regular expression). In our concrete example we have 
+  (with respect to a character). In our concrete example we have 
   @{term "X\<^isub>1 \<Turnstile>c\<Rightarrow> X\<^isub>2"}, @{term "X\<^isub>1 \<Turnstile>d\<Rightarrow> X\<^isub>3"} with @{text d} being any 
   other character than @{text c}, and @{term "X\<^isub>3 \<Turnstile>d\<Rightarrow> X\<^isub>3"} for any @{text d}.
   
@@ -428,7 +428,7 @@
   \end{center}
 
   \noindent
-  where the pairs @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} stand for all transitions 
+  where the terms @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} stand for all transitions 
   @{term "Y\<^isub>i\<^isub>j \<Turnstile>c\<^isub>i\<^isub>j\<Rightarrow> X\<^isub>i"}. Our internal represeantation for the right-hand
   sides are sets of terms.
   There can only be finitely many such