Lines Matching defs:func
260 val (func,args) =
265 val _ = if not(is_const func)
266 then (print_term func; print " is not a constant\n";
335 val (func,args) =
340 val _ = if not(is_const func)
341 then (print_term func; print " is not a constant\n";
358 andalso aconv (rator t2) func
359 andalso not(occurs_in func b)
360 andalso not(occurs_in func t1)
361 andalso not(occurs_in func (rand t2)))
366 val thm = ISPECL[func,fb,f1,f2] Rec_INTRO
396 else if occurs_in func rt
397 then (print "definition of: "; print_term func;
410 val (func,args) = dest_comb l
411 val is_recursive = Lib.can (find_term (aconv func)) r
562 let val (is_recursive,func,args,const_eq_comb) = toComb def
565 (func,(is_recursive,def,anf,const_eq_comb))::env