Lines Matching refs:function
118 (* These take as argument a thm_tactic, a function which takes a *)
183 fun TACTIC_ERR{function,message} =
185 origin_function = function,
188 fun failwith function =
190 print_string ("Failure in dep_rewrite: "^function^"\n")
192 raise TACTIC_ERR{function = function,message = "Failure in dep_rewrite"});
303 (* APPLY_IMP_THEN ttac th is a dependent rewriting function, *)
395 (* TAC_DEP turns a tactic into a dependent rewriting function. *)
405 (* DEP_TAC turns a dependent rewriting function into a tactic. *)