--- a/thys/Re1.thy	Thu Feb 26 12:51:02 2015 +0000
+++ b/thys/Re1.thy	Thu Feb 26 16:35:10 2015 +0000
@@ -345,22 +345,30 @@
 apply (rule ValOrd.intros(2))
 apply metis
 apply(simp)
+(* ALT case *)
 apply(simp)
 apply(erule disjE)
 apply(simp)
 apply (metis POSIX_ALT_I1)
-apply(auto)
+(* *)
+apply(auto)[1]
+thm  POSIX_ALT_I1
 apply (metis POSIX_ALT_I1)
-apply(simp add: POSIX_def)
+apply(simp (no_asm) add: POSIX_def)
 apply(auto)[1]
-apply (metis Prf.intros(3))
-apply(rotate_tac 5)
+apply(rule Prf.intros(3))
+apply(simp only: POSIX_def)
+apply(rotate_tac 4)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(simp add: mkeps_flat)
 apply(auto)[1]
+thm Prf_flat_L nullable_correctness
 apply (metis Prf_flat_L nullable_correctness)
 apply(rule ValOrd.intros)
+apply(subst (asm) POSIX_def)
+apply(clarify)
+apply(drule_tac x="v2" in spec)
 by metis
 
 
@@ -401,8 +409,8 @@
 fun projval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 where
   "projval (CHAR d) c _ = Void"
-| "projval (ALT r1 r2) c (Left v1) = Left(projval r1 c v1)"
-| "projval (ALT r1 r2) c (Right v2) = Right(projval r2 c v2)"
+| "projval (ALT r1 r2) c (Left v1) = Left (projval r1 c v1)"
+| "projval (ALT r1 r2) c (Right v2) = Right (projval r2 c v2)"
 | "projval (SEQ r1 r2) c (Seq v1 v2) = 
      (if flat v1 = [] then Right(projval r2 c v2) 
       else if nullable r1 then Left (Seq (projval r1 c v1) v2)