src/HOL/UNITY/Simple/Reachability.thy

    apply (blast intro: Stable_INT Stable_reachable_EQ_R_AND_nmsg_0
                     Leadsto_reachability_AND_nmsg_0)+
 done
 
 lemma LeadsTo_final: "F \<in> UNIV LeadsTo final"
-apply (case_tac "E={}")
+apply (cases "E={}")
  apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
 apply (rule LeadsTo_final_E_empty, auto)
 done
 
 (* ------------------------------------ *)

               (- {} \<union> nmsg_eq 0 (v,w)))")
 apply blast+
 done
 
 lemma Stable_final: "F \<in> Stable final"
-apply (case_tac "E={}")
+apply (cases "E={}")
  prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
 apply (blast intro: Stable_final_E_empty)
 done
 
 end