Lines Matching refs:function
92 (* last arguments in the pattern will be instances of a function symbol
257 (* Version that defines function(s). *)
346 Make a new recursive function definition.
473 (* Internal function: *)
495 (* Internal function: GTAC *)
515 (* Internal function: TACF *)
544 (* TACF is a strictly local function, used only to define TACS, below. *)
566 (* Internal function: TACS *)
580 (* TACS is a strictly local function, used only in INDUCT_THEN. *)
590 (* Internal function: GOALS *)
597 (* GOALS is a strictly local function, used only in INDUCT_THEN. *)
610 (* Internal function: GALPH *)
633 (* Internal function: GALPHA *)
706 (* Internal function: UNIQUENESS *)
708 (* This function derives uniqueness from unique existence: *)
745 (* Internal function: DEPTH_FORALL_CONV *)
760 (* Internal function: CONJS_CONV *)
775 (* Internal function: CONJS_SIMP *)
797 (* Internal function: T_AND_CONV *)
809 (* Internal function: GENL_T *)
827 (* Internal function: SIMP_CONV *)
865 (* Internal function: HYP_SIMP *)
904 (* Internal function: ANTE_ALL_CONV *)
923 (* Internal function: CONCL_SIMP *)
1000 (* Internal function: NOT_ALL_THENC *)
1022 (* Internal function: BASE_CONV *)
1041 (* Internal function: STEP_CONV *)
1065 (* Internal function: NOT_IN_CONV *)
1099 (* Internal function: STEP_SIMP *)
1125 (* Internal function: DISJ_CHAIN *)
1411 (* Internal function: list_variant *)
1429 (* Internal function: prove_const_one_one. *)
1431 (* This function proves that a single constructor of a recursive type is *)
1451 (* Basic strategy is to use a function
1574 (* Basic strategy is to define a function over the type such that
1582 particular, the type of the function will be
1584 The encoding of the function will be such that it is true iff the
1591 When function f is defined, it is then easy to distinguish any
1648 mk_num generates the function corresponding to number n. The abstraction