--- a/thys/Re1.thy	Thu Feb 26 16:35:10 2015 +0000
+++ b/thys/Re1.thy	Wed Mar 04 19:34:47 2015 +0000
@@ -346,6 +346,7 @@
 apply metis
 apply(simp)
 (* ALT case *)
+thm mkeps.simps
 apply(simp)
 apply(erule disjE)
 apply(simp)
@@ -361,6 +362,7 @@
 apply(rotate_tac 4)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+thm mkeps_flat
 apply(simp add: mkeps_flat)
 apply(auto)[1]
 thm Prf_flat_L nullable_correctness
@@ -369,7 +371,7 @@
 apply(subst (asm) POSIX_def)
 apply(clarify)
 apply(drule_tac x="v2" in spec)
-by metis
+by simp
 
 
 section {* Derivatives *}
@@ -727,6 +729,7 @@
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
 (* EMPTY case *)
+apply(simp)
 apply(erule ValOrd.cases)
 apply(simp_all)[8]
 (* CHAR case *)