diff -r 59bad592a009 -r 80218dddbb15 thys/ReTest.thy
--- a/thys/ReTest.thy	Wed Feb 24 21:08:35 2016 +0000
+++ b/thys/ReTest.thy	Thu Feb 25 12:17:31 2016 +0000
@@ -1152,6 +1152,19 @@
  L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC32 s' r r'" and
  L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow>  x \<noteq> [] \<longrightarrow> \<not>PC42 s s' r r'"
 apply(auto simp add: PC32_def PC42_def)[1]
+apply(simp add: Sequ_def)
+apply (metis nullable_correctness)
+apply(auto simp add: PC32_def PC42_def Sequ_def)[1]
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+apply(simp add: Cons_eq_append_conv)
+apply(auto)[1]
+defer
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def nullable_correctness)[1]
+apply (metis append_Cons append_assoc hd_Cons_tl list.discI list.inject)
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
 oops
 
 definition 
@@ -1663,6 +1676,7 @@
 apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
 apply(drule mp)
 apply(simp)
+
 apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2)
 apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
 apply (metis NPrf_imp_Prf Prf.intros(1))