src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy

 apply assumption
 (* IH *)
 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
 
 (* a~: act B; a~: act A *)
-apply (fastsimp intro!: ext_is_act simp: externals_of_par)
+apply (fastforce intro!: ext_is_act simp: externals_of_par)
 done
 
 declare FiniteConc [simp]
 
 declare FilterConc [simp del]

 back
 apply assumption
 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
 
 (* Case a~:A, a~:B *)
-apply (fastsimp intro!: ext_is_act simp: externals_of_par)
+apply (fastforce intro!: ext_is_act simp: externals_of_par)
 done
 
 
 subsection" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"