equal
deleted
inserted
replaced
199 val succeed = METHOD (K all_tac); |
199 val succeed = METHOD (K all_tac); |
200 |
200 |
201 |
201 |
202 (* shuffle *) |
202 (* shuffle *) |
203 |
203 |
204 fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 1))); |
204 fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1))); |
205 fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1))); |
205 fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1))); |
206 |
206 |
207 |
207 |
208 (* insert *) |
208 (* insert *) |
209 |
209 |