--- a/Myhill_1.thy	Thu Jan 27 12:35:06 2011 +0000
+++ b/Myhill_1.thy	Thu Jan 27 16:58:11 2011 +0000
@@ -1,5 +1,5 @@
 theory Myhill_1
-  imports Main List_Prefix Prefix_subtract
+  imports Main List_Prefix Prefix_subtract Prelude
 begin
 
 (*
@@ -26,15 +26,20 @@
 
 section {* Preliminary definitions *}
 
-text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *}
+types lang = "string set"
+
+text {* 
+  Sequential composition of two languages @{text "L1"} and @{text "L2"} 
+*}
+
 definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 where 
   "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
 
 text {* Transitive closure of language @{text "L"}. *}
 inductive_set
-  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
-  for L :: "string set"
+  Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
+  for L 
 where
   start[intro]: "[] \<in> L\<star>"
 | step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" 
@@ -193,7 +198,7 @@
   *}
 lemma folds_alt_simp [simp]:
   "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"
-apply (rule set_ext, simp add:folds_def)
+apply (rule set_eq_intro, simp add:folds_def)
 apply (rule someI2_ex, erule finite_imp_fold_graph)
 by (erule fold_graph.induct, auto)
 
@@ -206,7 +211,7 @@
   @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}.
 *}
 definition
-  str_eq_rel ("\<approx>_")
+  str_eq_rel ("\<approx>_" [100] 100)
 where
   "\<approx>Lang \<equiv> {(x, y).  (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}"