Lines Matching refs:function
321 (* The function p:term->bool is a predicate which will be *)
354 (* fnn = a function which, when applied to a rewriting conversion *)
359 (* pf = a function which maps |- tm to [|- t1;...;|- tj] where each *)
454 (* function decides which equations to use by performing a loop analysis on *)
459 (* The algorithms used for loop analysis in this function are extremely *)
463 (* Amongst other things, the internal function "graph_of_term' rearranges the*)
465 (* gives them priority over the internal lines when the function is *)
648 (* function decides which equations to use by performing a loop analysis on *)
692 (* x1 and x2 do not appear free in t but x3 does, the function will fail; it *)
957 (* possible the function will fail. It is also possible for the function to *)
987 (* conjunct, it is unchanged. After rewriting the function decides which of *)
991 (* Suppose the function decides to unwind the lines li1,...,lik using the *)
1043 (* possible the function will fail. It is also possible for the function to *)
1071 (* conjunct, it is unchanged. After rewriting the function decides which of *)
1075 (* Suppose the function decides to unwind the lines li1,...,lik using the *)