--- a/Myhill_2.thy	Mon Feb 07 13:17:01 2011 +0000
+++ b/Myhill_2.thy	Mon Feb 07 20:30:10 2011 +0000
@@ -1,5 +1,5 @@
 theory Myhill_2
-  imports Myhill_1
+  imports Myhill_1 List_Prefix Prefix_subtract
 begin
 
 section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
@@ -7,15 +7,15 @@
 subsection {* The scheme*}
 
 text {* 
-  The following convenient notation @{text "x \<approx>Lang y"} means:
+  The following convenient notation @{text "x \<approx>A y"} means:
   string @{text "x"} and @{text "y"} are equivalent with respect to 
-  language @{text "Lang"}.
+  language @{text "A"}.
   *}
 
 definition
   str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
 where
-  "x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)"
+  "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
 
 text {*
   The main lemma (@{text "rexp_imp_finite"}) is proved by a structural induction over regular expressions.