diff -r f754a10875c7 -r c840a99a3e05 thys/SpecExt.thy
--- a/thys/SpecExt.thy	Tue Oct 10 11:31:47 2017 +0100
+++ b/thys/SpecExt.thy	Wed Oct 25 12:18:44 2017 +0100
@@ -71,7 +71,7 @@
 lemma Der_Sequ [simp]:
   shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
 unfolding Der_def Sequ_def
-by (auto simp add: Cons_eq_append_conv)
+  by (auto simp add: Cons_eq_append_conv)
 
 
 section {* Kleene Star for Languages *}
@@ -237,9 +237,9 @@
 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 | "L (STAR r) = (L r)\<star>"
-| "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)"
+| "L (UPNTIMES r n) = (\<Union>i\<in>{..n} . (L r) \<up> i)"
 | "L (NTIMES r n) = (L r) \<up> n"
-| "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)"
+| "L (FROMNTIMES r n) = (\<Union>i\<in>{n..} . (L r) \<up> i)"
 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" 
 
 section {* Nullable, Derivatives *}
@@ -368,7 +368,6 @@
    (simp_all add: Ders_def der_correctness Der_def)
 
 
-
 section {* Values *}
 
 datatype val = 
@@ -1422,8 +1421,12 @@
     apply(drule_tac x="vs" in meta_spec)
     apply(simp)
      apply(drule meta_mp)
-      apply (smt L.simps(10) Posix1(1) Posix1(2) Posix_NMTIMES1.hyps(4) UN_E append.right_neutral
-             append_eq_append_conv2 diff_Suc_1 val.inject(5))
+      apply(drule Posix1(1))
+      apply(drule Posix1(1))
+      apply(drule Posix1(1))
+      apply(frule Posix1(1))
+      apply(simp)
+    using Posix_NMTIMES1.hyps(4) apply force
      apply (metis L.simps(10) Posix1(1) UN_E append_Nil2 append_self_conv2)
     by (metis One_nat_def Posix1(1) Posix_NMTIMES1.hyps(8) append.right_neutral append_Nil)      
   moreover