--- a/Paper/Paper.thy	Thu Apr 21 12:07:11 2011 +0000
+++ b/Paper/Paper.thy	Thu Apr 21 22:41:15 2011 +0000
@@ -465,8 +465,8 @@
   \noindent
   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"}. In terms of finite automata, every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
-  corresponds very roughly to a state whose name is @{text X\<^isub>i} and its predecessor states 
+  X\<^isub>i"}. If viewed as an automaton, then every equation @{text "X\<^isub>i = rhs\<^isub>i"} in this system
+  corresponds roughly to a state whose name is @{text X\<^isub>i} and its predecessor states 
   are the @{text "Y\<^isub>i\<^isub>j"}; the @{text "c\<^isub>i\<^isub>j"} are the labels of the transitions from these 
   predecessor states to @{text X\<^isub>i}. In our initial equation system there can only be
   finitely many terms of the form @{text "(Y\<^isub>i\<^isub>j, CHAR c\<^isub>i\<^isub>j)"} in a right-hand side