diff -r bba9c80735f9 -r f901a26bf1ac Myhill_1.thy
--- a/Myhill_1.thy	Tue Feb 08 15:50:26 2011 +0000
+++ b/Myhill_1.thy	Tue Feb 08 15:59:47 2011 +0000
@@ -528,13 +528,6 @@
 definition 
   "rexp_of rhs X \<equiv> \<Uplus> {r. Trn X r \<in> rhs}"
 
-text {* 
-  The following @{text "lam_of rhs"} returns all pure regular expression trns in @{text "rhs"}.
-*}
-
-definition
-  "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"
-
 text {*
   The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"}
   using @{text "ALT"} to form a single regular expression. 
@@ -1253,8 +1246,6 @@
   def A \<equiv> "arden_variate X xrhs"
   have "?P (rexp_of_lam A)"
   proof -
-    thm lam_of_def
-    thm rexp_of_lam_def
     have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in>  A})"
     proof(rule rexp_of_lam_eq_lam_set)
       show "finite A" 
@@ -1265,7 +1256,7 @@
     qed
     also have "\<dots> = L A"
     proof-
-      have "lam_of A = A"
+      have "{Lam r | r. Lam r \<in> A} = A"
       proof-
         have "classes_of A = {}" using Inv_ES ES_single
 	  unfolding A_def
@@ -1273,9 +1264,9 @@
                        self_contained_def Inv_def lefts_of_def) 
         thus ?thesis
 	  unfolding A_def
-          by (auto simp only:lam_of_def classes_of_def, case_tac x, auto)
+          by (auto simp only: classes_of_def, case_tac x, auto)
       qed
-      thus ?thesis unfolding lam_of_def by simp
+      thus ?thesis by simp
     qed
     also have "\<dots> = X"
     unfolding A_def