equal
deleted
inserted
replaced
183 (fn [] => assm_tac ctxt |
183 (fn [] => assm_tac ctxt |
184 | [fact] => solve_tac [fact] |
184 | [fact] => solve_tac [fact] |
185 | _ => K no_tac)); |
185 | _ => K no_tac)); |
186 |
186 |
187 fun finish immed ctxt = |
187 fun finish immed ctxt = |
188 METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac)); |
188 METHOD (K ((if immed then all_assm_tac ctxt else all_tac) THEN flexflex_tac ctxt)); |
189 |
189 |
190 end; |
190 end; |
191 |
191 |
192 |
192 |
193 (* rule etc. -- single-step refinements *) |
193 (* rule etc. -- single-step refinements *) |
203 local |
203 local |
204 |
204 |
205 fun gen_rule_tac tac ctxt rules facts = |
205 fun gen_rule_tac tac ctxt rules facts = |
206 (fn i => fn st => |
206 (fn i => fn st => |
207 if null facts then tac rules i st |
207 if null facts then tac rules i st |
208 else Seq.maps (fn rule => (tac o single) rule i st) (Drule.multi_resolves facts rules)) |
208 else |
|
209 Seq.maps (fn rule => (tac o single) rule i st) |
|
210 (Drule.multi_resolves (SOME ctxt) facts rules)) |
209 THEN_ALL_NEW Goal.norm_hhf_tac ctxt; |
211 THEN_ALL_NEW Goal.norm_hhf_tac ctxt; |
210 |
212 |
211 fun gen_arule_tac tac ctxt j rules facts = |
213 fun gen_arule_tac tac ctxt j rules facts = |
212 EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac); |
214 EVERY' (gen_rule_tac tac ctxt rules facts :: replicate j assume_tac); |
213 |
215 |