Lines Matching defs:func
204 val (func,args) =
208 val _ = if not(is_const func)
209 then (print_term func; print " is not a constant\n";
253 val (func,args) = dest_comb lt
264 andalso aconv (rator t2) func
265 andalso not(occurs_in func b)
266 andalso not(occurs_in func t1)
267 andalso not(occurs_in func (rand t2)))
272 val thm = ISPECL[func,fb,f1,f2] rec_INTRO
304 else if occurs_in func rt
305 then (print "definition of: "; print_term func;
318 val (func,args) = dest_comb l
319 val is_recursive = Lib.can (find_term (aconv func)) r
331 let val (is_recursive,func,args,const_eq_comb) = toComb def
333 (func,(is_recursive,def,const_eq_comb))::env