--- a/Myhill_1.thy	Fri Feb 11 13:30:37 2011 +0000
+++ b/Myhill_1.thy	Sun Feb 13 10:36:53 2011 +0000
@@ -184,10 +184,8 @@
 qed
 
 
-
 section {* A modified version of Arden's lemma *}
 
-
 text {*  A helper lemma for Arden *}
 
 lemma arden_helper:
@@ -306,7 +304,6 @@
 done
 
 
-
 section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
 
 
@@ -349,10 +346,8 @@
 unfolding finals_def quotient_def
 by auto
 
-
 section {* Equational systems *}
 
-
 text {* The two kinds of terms in the rhs of equations. *}
 
 datatype rhs_item = 
@@ -499,8 +494,6 @@
 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"},