src/HOL/Statespace/DistinctTreeProver.thy

         by (auto split: split_if_asm)
     next
       case None
       with l'_l Some x_l_Some del
       show ?thesis
-        by (fastsimp split: split_if_asm)
+        by (fastforce split: split_if_asm)
     qed
   next
     case None
     note x_l_None = this
     show ?thesis

       with Node.hyps
       have "set_of r' \<subseteq> set_of r"
         by simp
       with Some x_l_None del
       show ?thesis
-        by (fastsimp split: split_if_asm)
+        by (fastforce split: split_if_asm)
     next
       case None
       with x_l_None del
       show ?thesis
-        by (fastsimp split: split_if_asm)
+        by (fastforce split: split_if_asm)
     qed
   qed
 qed
 
 lemma delete_Some_all_distinct: 

       from delete_Some_set_of [OF Some]
       have "set_of r' \<subseteq> set_of r".
       
       with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r
       show ?thesis
-        by fastsimp
+        by fastforce
     next
       case None
       with l'_l dist_l'  x_l_Some del d dist_l_r dist_r
       show ?thesis
-        by fastsimp
+        by fastforce
     qed
   next
     case None
     note x_l_None = this
     show ?thesis

         by simp
       from delete_Some_set_of [OF Some]
       have "set_of r' \<subseteq> set_of r".
       with Some dist_r' x_l_None del dist_l d dist_l_r
       show ?thesis
-        by fastsimp
+        by fastforce
     next
       case None
       with x_l_None del dist_l dist_r d dist_l_r
       show ?thesis
-        by (fastsimp split: split_if_asm)
+        by (fastforce split: split_if_asm)
     qed
   qed
 qed
 
 lemma delete_None_set_of_conv: "delete x t = None = (x \<notin> set_of t)"