--- a/Closures.thy	Wed Aug 03 17:08:31 2011 +0000
+++ b/Closures.thy	Fri Aug 05 05:34:11 2011 +0000
@@ -142,6 +142,9 @@
   
 subsection {* Closure under left-quotients *}
 
+abbreviation
+  "Ders_set A B \<equiv> \<Union>s \<in> A. Ders s B"
+
 lemma closure_left_quotient:
   assumes "regular A"
   shows "regular (Ders_set B A)"
@@ -150,7 +153,7 @@
   have fin: "finite (pders_set B r)" by (rule finite_pders_set)
   
   have "Ders_set B (lang r) = (\<Union> lang ` (pders_set B r))"
-    by (simp add: Ders_set_pders_set)
+    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
     by simp