--- a/Closures.thy	Tue Aug 09 22:14:41 2011 +0000
+++ b/Closures.thy	Tue Aug 09 22:15:11 2011 +0000
@@ -143,21 +143,21 @@
 subsection {* Closure under left-quotients *}
 
 abbreviation
-  "Ders_set A B \<equiv> \<Union>s \<in> A. Ders s B"
+  "Ders_lang A B \<equiv> \<Union>s \<in> A. Ders s B"
 
 lemma closure_left_quotient:
   assumes "regular A"
-  shows "regular (Ders_set B A)"
+  shows "regular (Ders_lang B A)"
 proof -
   from assms obtain r::"'a rexp" where eq: "lang r = A" by auto
-  have fin: "finite (pders_set B r)" by (rule finite_pders_set)
+  have fin: "finite (pders_lang B r)" by (rule finite_pders_lang)
   
-  have "Ders_set B (lang r) = (\<Union> lang ` (pders_set B r))"
+  have "Ders_lang B (lang r) = (\<Union> lang ` (pders_lang B r))"
     by (simp add: Ders_pders)
-  also have "\<dots> = lang (\<Uplus>(pders_set B r))" using fin by simp
-  finally have "Ders_set B A = lang (\<Uplus>(pders_set B r))" using eq
+  also have "\<dots> = lang (\<Uplus>(pders_lang B r))" using fin by simp
+  finally have "Ders_lang B A = lang (\<Uplus>(pders_lang B r))" using eq
     by simp
-  then show "regular (Ders_set B A)" by auto
+  then show "regular (Ders_lang B A)" by auto
 qed