--- a/Myhill_1.thy	Fri Feb 04 13:33:18 2011 +0000
+++ b/Myhill_1.thy	Fri Feb 04 22:54:29 2011 +0000
@@ -210,7 +210,6 @@
   than the level of regular expression. 
 *}
 
-
 lemma ardens_helper:
   assumes eq: "X = X ;; A \<union> B"
   shows "X = X ;; (A \<up> Suc n) \<union> (\<Union>m\<in>{0..n}. B ;; (A \<up> m))"