diff -r 652861c9473f -r c616ec6b1e3c thys/Re1.thy
--- a/thys/Re1.thy	Mon Jan 19 09:55:58 2015 +0000
+++ b/thys/Re1.thy	Wed Jan 21 12:32:17 2015 +0000
@@ -133,7 +133,7 @@
 using assms
 apply(induct)
 apply(auto)
-done
+oops
 
 
 section {* Posix definition *}
@@ -211,6 +211,7 @@
 apply(auto)
 apply (metis ValOrd.intros(1))
 apply (rule ValOrd.intros(2))
+oops
 
 lemma POSIX_ALT2:
   assumes "POSIX (Left v1) (ALT r1 r2)"
@@ -593,6 +594,7 @@
 apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply(case_tac "c = c'")
@@ -600,8 +602,10 @@
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply (metis Prf.intros(5))
+apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
+apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[5]
 apply (metis Prf.intros(2))