--- a/thys/RegLangs.thy	Sat Feb 23 21:52:06 2019 +0000
+++ b/thys/RegLangs.thy	Wed Mar 13 10:36:29 2019 +0000
@@ -193,6 +193,8 @@
   shows "ders (s1 @ s2) r = ders s2 (ders s1 r)"
   by (induct s1 arbitrary: s2 r) (auto)
 
-
+lemma ders_snoc:
+  shows "ders (s @ [c]) r = der c (ders s r)"
+  by (simp add: ders_append)
 
 end
\ No newline at end of file