--- a/Myhill_1.thy	Sun Jan 30 17:24:37 2011 +0000
+++ b/Myhill_1.thy	Mon Jan 31 12:54:31 2011 +0000
@@ -34,7 +34,7 @@
 
 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" (infixr ";;" 100)
 where 
-  "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+  "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}"
 
 text {* 
   Transitive closure of language @{text "L"}. 
@@ -691,7 +691,7 @@
   have "finite ((snd \<circ> the_Trn) ` items_of rhs X)" using finite_items_of[OF finite] by auto
   thus ?thesis
     apply (auto simp:rexp_of_def Seq_def items_of_def)
-    apply (rule_tac x = s1 in exI, rule_tac x = s2 in exI, auto)
+    apply (rule_tac x = "s\<^isub>1" in exI, rule_tac x = "s\<^isub>2" in exI, auto)
     by (rule_tac x= "Trn X r" in exI, auto simp:Seq_def)
 qed
 
@@ -707,7 +707,9 @@
 lemma [simp]:
   " L (attach_rexp r xb) = L xb ;; L r"
 apply (cases xb, auto simp:Seq_def)
-by (rule_tac x = "s1 @ s1a" in exI, rule_tac x = s2a in exI,auto simp:Seq_def)
+apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI)
+apply(auto simp: Seq_def)
+done
 
 lemma lang_of_append_rhs:
   "L (append_rhs_rexp rhs r) = L rhs ;; L r"
@@ -1211,8 +1213,8 @@
   by (auto simp:finals_def quotient_def)   
 
 theorem hard_direction: 
-  assumes finite_CS: "finite (UNIV // (\<approx>Lang))"
-  shows   "\<exists> (reg::rexp). Lang = L reg"
+  assumes finite_CS: "finite (UNIV // \<approx>Lang)"
+  shows   "\<exists> (r::rexp). Lang = L r"
 proof -
   have "\<forall> X \<in> (UNIV // (\<approx>Lang)). \<exists> (reg::rexp). X = L reg" 
     using finite_CS every_eqcl_has_reg by blast