equal
deleted
inserted
replaced
373 (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions))) |
373 (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions))) |
374 |> Proof.refine_singleton (Method.primitive_text (K I))) oo |
374 |> Proof.refine_singleton (Method.primitive_text (K I))) oo |
375 prepare_common prepare_name prepare_sort prepare_term prepare_thm o apfst (apfst (apsnd SOME)); |
375 prepare_common prepare_name prepare_sort prepare_term prepare_thm o apfst (apfst (apsnd SOME)); |
376 |
376 |
377 fun prepare_solve prepare_name prepare_typ prepare_sort prepare_thm tacs = |
377 fun prepare_solve prepare_name prepare_typ prepare_sort prepare_thm tacs = |
378 (fn (goals, after_qed, _, lthy) => |
378 (fn (goals, after_qed, definitions, lthy) => |
379 lthy |
379 lthy |
380 |> after_qed (map2 (single oo Goal.prove lthy [] []) goals (tacs (length goals)))) oo |
380 |> after_qed (map2 (fn goal => fn tac => [Goal.prove lthy [] [] goal |
|
381 (fn (ctxtprems as {context = ctxt, prems = _}) => |
|
382 unfold_thms_tac ctxt definitions THEN tac ctxtprems)]) |
|
383 goals (tacs (length goals)))) oo |
381 prepare_common prepare_name prepare_typ prepare_sort prepare_thm; |
384 prepare_common prepare_name prepare_typ prepare_sort prepare_thm; |
382 |
385 |
383 in |
386 in |
384 |
387 |
385 val lift_bnf_cmd = |
388 val lift_bnf_cmd = |