File ‹method_util.ML›

(*  Title:      ML_Utils/method_util.ML
    Author:     Kevin Kappelmann

Method utilities.
*)
signature METHOD_UTIL =
sig
  val METHOD_CONTEXT : (thm list -> 'a -> tactic) -> 'a -> Method.method
  val METHOD_CONTEXT' : (thm list -> 'a -> int -> tactic) -> 'a -> Method.method
end

structure Method_Util : METHOD_UTIL =
struct

fun METHOD_CONTEXT tac x = METHOD (fn thms => tac thms x)
fun METHOD_CONTEXT' tac x = METHOD (fn thms => HEADGOAL (tac thms x))

end