diff -r 59bad592a009 -r 80218dddbb15 thys/ReStar.thy
--- a/thys/ReStar.thy	Wed Feb 24 21:08:35 2016 +0000
+++ b/thys/ReStar.thy	Thu Feb 25 12:17:31 2016 +0000
@@ -1224,10 +1224,13 @@
 using assms
 apply(induct c r arbitrary: s v rule: der.induct)
 apply(auto)
+(* NULL case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
+(* EMPTY case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
+(* CHAR case *)
 apply(case_tac "c = c'")
 apply(simp)
 apply(erule PMatch.cases)
@@ -1236,6 +1239,7 @@
 apply(simp)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
+(* ALT case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 apply (metis PMatch.intros(3))
@@ -1247,6 +1251,7 @@
 apply(case_tac "nullable r1")
 apply(simp)
 prefer 2
+(* not-nullbale case *)
 apply(simp)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
@@ -1261,9 +1266,14 @@
 (* nullable case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
+(* left case *)
 apply(clarify)
 apply(erule PMatch.cases)
 apply(simp_all)[4]
+prefer 2
+apply(clarify)
+prefer 2
+apply(clarify)
 apply(clarify)
 apply(simp (no_asm))
 apply(subst append.simps(2)[symmetric])
@@ -1275,9 +1285,7 @@
 apply(auto)[1]
 apply(simp add: der_correctness Der_def)
 apply metis
-apply(simp)
-(* interesting case *)
-apply(clarify)
+(* right interesting case *)
 apply(clarify)
 apply(simp)
 apply(subst (asm) L.simps(4)[symmetric])