--- a/thys/ReStar.thy	Wed Mar 02 04:13:25 2016 +0000
+++ b/thys/ReStar.thy	Wed Mar 02 14:06:13 2016 +0000
@@ -24,18 +24,13 @@
 by (simp_all add: Sequ_def)
 
 
-section {* Semantic Derivatives of Languages *}
+section {* Semantic Derivative of Languages *}
 
 definition
   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
 where
   "Der c A \<equiv> {s. [c] @ s \<in> A}"
 
-definition 
-  Ders :: "string \<Rightarrow> string set \<Rightarrow> string set"
-where  
-  "Ders s A \<equiv> {s' | s'. s @ s' \<in> A}"
-
 lemma Der_null [simp]:
   shows "Der c {} = {}"
 unfolding Der_def
@@ -167,12 +162,6 @@
 apply(simp_all add: nullable_correctness)
 done
 
-lemma ders_correctness:
-  shows "L (ders s r) = Ders s (L r)"
-apply(induct s arbitrary: r) 
-apply(simp_all add: der_correctness Der_def Ders_def)
-done
-
 
 section {* Values *}