Lines Matching refs:function
15 fun COND_REWR_ERR {function,message} =
17 origin_function = function,
114 then raise COND_REWR_ERR{function="MATCH_SUBS1",
151 (* fn is a search function which returns a list of matches in the format *)
152 (* of the list returned by the system function match. *)
158 (* This tactic uses the search function fn to find any matches of Q in *)
181 then raise COND_REWR_ERR{function="COND_REWR_TAC", message="no match"}
189 (raise COND_REWR_ERR {function="COND_REWR_TAC",
249 (* fn is a function attempting to match the lhs of the conclusion of th *)
251 (* this function is used to instantiate the input theorem. the resulting *)
261 then raise COND_REWR_ERR{function="COND_REWR_CONV", message="no match"}
269 (raise COND_REWR_ERR {function="COND_REWR_CONV",