--- a/thys/Spec.thy	Wed Aug 15 13:48:57 2018 +0100
+++ b/thys/Spec.thy	Thu Aug 16 01:12:00 2018 +0100
@@ -174,6 +174,11 @@
 by (induct s arbitrary: r)
    (simp_all add: Ders_def der_correctness Der_def)
 
+lemma ders_append:
+  shows "ders (s1 @ s2) r = ders s2 (ders s1 r)"
+  apply(induct s1 arbitrary: s2 r)
+  apply(auto)
+  done
 
 
 section {* Values *}