src/HOL/Unix/Unix.thy

   next
     case rmdir
     with root show ?thesis by cases auto
   next
     case readdir
-    with root show ?thesis by cases auto
+    with root show ?thesis by cases (simp (asm_lr))+
   qed
 qed
 
 text {*
   \medskip Apparently, file-system transitions are \emph{type-safe} in

             also from lookup have "\<dots> = lookup root (path @ [y])"
               by (simp only: lookup_append_some)
             also have "\<dots> \<noteq> None"
             proof -
               from ys obtain us u where rev_ys: "ys = us @ [u]"
-                by (cases ys rule: rev_cases) auto
+                by (cases ys rule: rev_cases) fastsimp+
               with tr path
               have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
                   lookup root ((path @ [y]) @ us) \<noteq> None"
                 by cases (auto dest: access_some_lookup)
               thus ?thesis by (blast dest!: lookup_some_append)