--- a/Myhill.thy	Sat Feb 05 09:54:52 2011 +0000
+++ b/Myhill.thy	Sat Feb 05 13:56:50 2011 +0000
@@ -35,7 +35,15 @@
 in which case, the string is rejected by situation \ref{case_end_reject} above.
 
 Given a language @{text "Lang"} and a string @{text "x"}, the equivalent class @{text "\<approx>Lang `` {x}"}
-corresponds to the state reached by processing @{text "x"} with the augmented automaton. 
+corresponds to the state reached by processing @{text "x"} with the augmented automaton. Since  
+@{text "\<approx>Lang `` {x}"} is defined for every @{text "x"}, it corresponds to the fact that 
+the processing of @{text "x"} will never get stuck.
+
+The most acquainted way to define a regular language @{text "Lang"} is by giving an automaton which
+recorgizes every string in @{text "Lang"}. Fig.\ref{fig_origin_auto} gives such a automaton, which 
+can be viewed as a way of assigning status to strings: for any given string @{text "x"}:
+
+
 
 \begin{figure}[h!]
 \centering

Binary file tphols-2011/myhill.pdf has changed