diff -r 212bfa431fa5 -r 79b37ef9505f Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Feb 16 06:51:58 2011 +0000
+++ b/Paper/Paper.thy	Wed Feb 16 12:25:53 2011 +0000
@@ -749,7 +749,7 @@
   that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
   and that the invariant holds for this equation. That means we 
   know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
-  this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties in the 
+  this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the 
   invariant and Lem.~???. Using the validity property for the equation @{text "X = rhs"},
   we can infer that @{term "rhss rhs \<subseteq> {X}"} and because the arden operation
   removes that @{text X} from @{text rhs}, that @{term "rhss (Arden X rhs) = {}"}.
@@ -804,16 +804,23 @@
   \end{center}
 
   \end{proof}
+
+
+  @{thm tag_str_ALT_def[where ?L1.0="A" and ?L2.0="B"]}
+
+  @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B"]}
+ 
+  @{thm tag_str_STAR_def[where ?L1.0="A"]}
 *}
 
 
 section {* Conclusion and Related Work *}
 
 text {*
-  In this paper we took the view that a regular language as one where there exists 
+  In this paper we took the view that a regular language is one where there exists 
   a regular expression that matches all its strings. For us it was important to find 
   out how far we can push this point of view. Having formalised the Myhill-Nerode
-  theorem means pushed very far. Having the Myhill-Nerode theorem means we can 
+  theorem means pushed quite far. Having the Myhill-Nerode theorem means we can 
   formalise much of the textbook results in this subject.