--- a/thys/ReStar.thy	Fri Mar 11 00:38:38 2016 +0000
+++ b/thys/ReStar.thy	Fri Mar 11 00:56:46 2016 +0000
@@ -212,8 +212,6 @@
   "\<turnstile> v : CHAR c"
 (*  "\<turnstile> vs : STAR r"*)
 
-
-
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
@@ -251,7 +249,6 @@
 apply (metis empty_iff list.set(1))
 by (metis concat.simps(2) list.simps(9) set_ConsD)
 
-
 lemma L_flat_Prf:
   "L(r) = {flat v | v. \<turnstile> v : r}"
 apply(induct r)
@@ -342,43 +339,8 @@
   shows "flat (injval r c v) = c # (flat v)"
 using assms
 apply(induct arbitrary: v rule: der.induct)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(simp)
-apply(case_tac "c = d")
-apply(simp)
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(simp)
-apply(case_tac "nullable r1")
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all (no_asm_use))[7]
-apply(auto)[1]
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(clarify)
-apply(simp only: injval.simps flat.simps)
-apply(auto)[1]
-apply (metis mkeps_flat)
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(simp)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)
+apply(auto elim!: Prf_elims split: if_splits)
+apply(metis mkeps_flat)
 apply(rotate_tac 2)
 apply(erule Prf.cases)
 apply(simp_all)[7]
@@ -433,7 +395,7 @@
 apply(induct r)
 apply(auto intro: PMatch.intros simp add: nullable_correctness Sequ_def)
 apply(subst append.simps(1)[symmetric])
-apply (rule PMatch.intros)
+apply(rule PMatch.intros)
 apply(auto)
 done