Lines Matching defs:func
288 let val (func,args) =
293 val _ = if not(is_const func)
294 then (print_term func; print " is not a constant\n";
356 val (func,args) =
361 val _ = if not(is_const func)
362 then (print_term func; print " is not a constant\n";
379 andalso aconv (rator t2) func
380 andalso not(occurs_in func b)
381 andalso not(occurs_in func t1)
382 andalso not(occurs_in func (rand t2)))
394 val th3 = SPEC func (MATCH_MP TOTAL_THM totalth)
398 (mk_comb(func,args),
402 mk_comb(func,mk_comb(f2,args)))))
418 else if occurs_in func rt
419 then (print "definition of: "; print_term func;
432 val (func,args) = dest_comb lt
585 let val (func,_) =
588 val _ = if not(is_const func)
592 CompileProg [th] func
654 val (func,args) = dest_comb l