--- a/Paper/Paper.thy	Tue Feb 15 12:01:29 2011 +0000
+++ b/Paper/Paper.thy	Tue Feb 15 14:17:31 2011 +0000
@@ -586,13 +586,15 @@
 
   \noindent
   Finially, we can define how an equational system should be solved. For this 
-  we will need to iterate the elimination of an equation until only one equation
+  we will need to iterate the process of eliminating equations until only one equation
   will be left in the system. However, we not just want to have any equation
-  as being the last one, but the one for which we want to calculate the regular 
-  expression. Therefore we define the iteration step so that it chooses an
-  equation with an equivalence class that is not @{text X}. This allows us to 
-  control, which equation will be the last. We use Hilbert's choice operator, 
-  written @{text SOME}, to choose an equation to be eliminated in @{text ES}.
+  as being the last one, but the one involving the equivalence class for 
+  which we want to calculate the regular 
+  expression. Let us suppose the equivalence class is @{text X}. 
+  Since @{text X} is the one to be solved, in every iteration step we have to pick an
+  equation to be eliminated that which is different from @{text X}. In this way 
+  @{text X} is kept to the final step. The choice is implemented by Hilbert's choice 
+  operator, written @{text SOME} in the definition below.
   
   \begin{center}
   \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
@@ -686,6 +688,10 @@
   @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
   \end{lemma}
 
+  \begin{proof} 
+  ???
+  \end{proof}
+
   \begin{lemma}
   @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
   \end{lemma}
@@ -705,6 +711,10 @@
   and @{term "invariant {(X, rhs)}"}.
   \end{lemma}
 
+  \begin{proof} 
+  ???
+  \end{proof}
+
   \noindent
   With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
   there exists a regular expression.
@@ -745,7 +755,7 @@
 
   \noindent
   Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"} 
-  as the regular expression that solves the goal.\qed
+  as the regular expression that is needed in the theorem.\qed
   \end{proof}
 *}