269 THEN Tactic.distinct_subgoals_tac; |
269 THEN Tactic.distinct_subgoals_tac; |
270 |
270 |
271 val intros_tac = gen_intros_tac ALLGOALS; |
271 val intros_tac = gen_intros_tac ALLGOALS; |
272 val try_intros_tac = gen_intros_tac TRYALL; |
272 val try_intros_tac = gen_intros_tac TRYALL; |
273 |
273 |
|
274 |
274 (* ML tactics *) |
275 (* ML tactics *) |
275 |
276 |
276 structure TacticData = Proof_Data |
277 structure ML_Tactic = Proof_Data |
277 ( |
278 ( |
278 type T = thm list -> tactic; |
279 type T = thm list -> tactic; |
279 fun init _ = undefined; |
280 fun init _ = undefined; |
280 ); |
281 ); |
281 |
282 |
282 val set_tactic = TacticData.put; |
283 val set_tactic = ML_Tactic.put; |
283 |
284 |
284 fun ml_tactic (txt, pos) ctxt = |
285 fun ml_tactic (txt, pos) ctxt = |
285 let |
286 let |
286 val ctxt' = ctxt |> Context.proof_map |
287 val ctxt' = ctxt |> Context.proof_map |
287 (ML_Context.expression pos |
288 (ML_Context.expression pos |
288 "fun tactic (facts: thm list) : tactic" |
289 "fun tactic (facts: thm list) : tactic" |
289 "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read pos txt)); |
290 "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read pos txt)); |
290 in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end; |
291 in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end; |
291 |
292 |
292 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt); |
293 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt); |
293 fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt); |
294 fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt); |
294 |
295 |
295 |
296 |