| changeset 60754 | 02924903a6fd |
| parent 59807 | 22bc39064290 |
| child 61076 | bdc1e2f0a86a |
--- a/src/HOL/Bali/AxCompl.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Bali/AxCompl.thy Sat Jul 18 20:54:56 2015 +0200 @@ -1370,7 +1370,7 @@ apply - apply (induct_tac "n") apply (tactic "ALLGOALS (clarsimp_tac @{context})") -apply (tactic {* dtac (Thm.permute_prems 0 1 @{thm card_seteq}) 1 *}) +apply (tactic {* dresolve_tac @{context} [Thm.permute_prems 0 1 @{thm card_seteq}] 1 *}) apply simp apply (erule finite_imageI) apply (simp add: MGF_asm ax_derivs_asm)