diff -r fc35eb54fdc9 -r fb08f41ca33d Myhill_1.thy --- 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 \ lang \ lang" (infixr ";;" 100) +definition + Seq :: "lang \ lang \ lang" (infixr ";;" 100) where "A ;; B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \ A \ s\<^isub>2 \ B}"