changeset 59498 | 50b60f501b05 |
parent 58963 | 26bf09b95dda |
child 60754 | 02924903a6fd |
--- a/src/ZF/UNITY/Constrains.thy Tue Feb 10 14:29:36 2015 +0100 +++ b/src/ZF/UNITY/Constrains.thy Tue Feb 10 14:48:26 2015 +0100 @@ -472,7 +472,7 @@ (EVERY [REPEAT (Always_Int_tac ctxt 1), REPEAT (etac @{thm Always_ConstrainsI} 1 ORELSE - resolve_tac [@{thm StableI}, @{thm stableI}, + resolve_tac ctxt [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1), rtac @{thm constrainsI} 1, (* Three subgoals *)