diff -r 37ab56205097 -r a9ebc410a5c8 Myhill_1.thy
--- a/Myhill_1.thy	Wed Feb 09 12:34:30 2011 +0000
+++ b/Myhill_1.thy	Thu Feb 10 05:57:56 2011 +0000
@@ -382,18 +382,18 @@
 text {* Transitions between equivalence classes *}
 
 definition 
-  transition :: "lang \<Rightarrow> rexp \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
+  transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100)
 where
-  "Y \<Turnstile>r\<Rightarrow> X \<equiv> Y ;; (L r) \<subseteq> X"
+  "Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<subseteq> X"
 
 text {* Initial equational system *}
 
 definition
   "init_rhs CS X \<equiv>  
       if ([] \<in> X) then 
-          {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}
+          {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}
       else 
-          {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"
+          {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"
 
 definition 
   "eqs CS \<equiv> {(X, init_rhs CS X) | X.  X \<in> CS}"
@@ -408,14 +408,14 @@
 *}
 
 fun 
-  attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
+  append_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item"
 where
-  "attach_rexp r (Lam rexp)   = Lam (SEQ rexp r)"
-| "attach_rexp r (Trn X rexp) = Trn X (SEQ rexp r)"
+  "append_rexp r (Lam rexp)   = Lam (SEQ rexp r)"
+| "append_rexp r (Trn X rexp) = Trn X (SEQ rexp r)"
 
 
 definition
-  "append_rhs_rexp rhs rexp \<equiv> (attach_rexp rexp) ` rhs"
+  "append_rhs_rexp rhs rexp \<equiv> (append_rexp rexp) ` rhs"
 
 definition 
   "arden_op X rhs \<equiv> 
@@ -624,7 +624,7 @@
 qed
 
 lemma [simp]:
-  "L (attach_rexp r xb) = L xb ;; L r"
+  "L (append_rexp r xb) = L xb ;; L r"
 apply (cases xb, 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)
@@ -635,7 +635,7 @@
 apply (auto simp:append_rhs_rexp_def image_def)
 apply (auto simp:Seq_def)
 apply (rule_tac x = "L xb ;; L r" in exI, auto simp add:Seq_def)
-by (rule_tac x = "attach_rexp r xb" in exI, auto simp:Seq_def)
+by (rule_tac x = "append_rexp r xb" in exI, auto simp:Seq_def)
 
 lemma classes_of_union_distrib:
   "classes_of A \<union> classes_of B = classes_of (A \<union> B)"
@@ -702,7 +702,7 @@
         and "clist \<in> Y"
         using decom "(1)" every_eqclass_has_transition by blast
       hence 
-        "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}"
+        "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>c\<Rightarrow> X}"
         unfolding transition_def
 	using "(1)" decom
         by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def)