--- a/Derivatives.thy	Thu Jul 28 14:22:10 2011 +0000
+++ b/Derivatives.thy	Thu Jul 28 17:52:36 2011 +0000
@@ -66,8 +66,8 @@
     apply(auto simp add: Cons_eq_append_conv)
     done
     
-  have "Der c (A\<star>) = Der c ({[]} \<union> A \<cdot> A\<star>)"
-    by (simp only: star_cases[symmetric])
+  have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})"
+    by (simp only: star_unfold_left[symmetric])
   also have "... = Der c (A \<cdot> A\<star>)"
     by (simp only: Der_union Der_one) (simp)
   also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))"
@@ -157,7 +157,7 @@
   pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
 where
   "pders [] r = {r}"
-| "pders (c # s) r = (\<Union>r'\<in> (pder c r). (pders s r'))"
+| "pders (c # s) r = \<Union> (pders s) ` (pder c r)"
 
 abbreviation
   "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"