--- a/Myhill_1.thy	Wed Feb 02 15:43:22 2011 +0000
+++ b/Myhill_1.thy	Thu Feb 03 05:38:47 2011 +0000
@@ -32,7 +32,8 @@
   Sequential composition of two languages @{text "L1"} and @{text "L2"} 
 *}
 
-definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)
+definition 
+  Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)
 where 
   "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"