diff -r 9c4daf15261c -r 2bb4a8d0111d src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Fri May 16 20:44:51 2025 +0200 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Sun May 18 14:33:01 2025 +0000 @@ -1188,7 +1188,7 @@ apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) \ \35 subgoals left\ apply(tactic \TRYALL(EVERY'[resolve_tac \<^context> [disjI1], - resolve_tac \<^context> [subset_trans], + resolve_tac \<^context> @{thms subset_trans}, eresolve_tac \<^context> @{thms Graph3}, force_tac \<^context>, assume_tac \<^context>])\)