Lines Matching refs:list
50 val FIRST_CONSEQ_CONV : conseq_conv list -> conseq_conv;
51 val EVERY_CONSEQ_CONV : conseq_conv list -> conseq_conv;
69 val ASM_CONSEQ_CONV_TAC : (thm list -> directed_conseq_conv) -> tactic
125 a theorem "|- t' ==> t" in the preprocessed strengthen list. Then CONSEQ_TOP_REWRITE_CONV
142 val CONSEQ_TOP_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv;
143 val CONSEQ_TOP_HO_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv;
149 val CONSEQ_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv;
150 val CONSEQ_HO_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv;
151 val ONCE_CONSEQ_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv;
152 val ONCE_CONSEQ_HO_REWRITE_CONV : (thm list * thm list * thm list) -> directed_conseq_conv;
154 val CONSEQ_REWRITE_TAC : (thm list * thm list * thm list) -> tactic;
155 val CONSEQ_HO_REWRITE_TAC : (thm list * thm list * thm list) -> tactic;
156 val ONCE_CONSEQ_REWRITE_TAC : (thm list * thm list * thm list) -> tactic;
157 val ONCE_CONSEQ_HO_REWRITE_TAC : (thm list * thm list * thm list) -> tactic;
159 val CONSEQ_TOP_REWRITE_TAC : (thm list * thm list * thm list) -> tactic;
160 val CONSEQ_TOP_HO_REWRITE_TAC : (thm list * thm list * thm list) -> tactic;
166 val LIST_GEN_IMP : term list -> thm -> thm;
168 val LIST_GEN_EQ : term list -> thm -> thm;
170 val LIST_EXISTS_INTRO_IMP : term list -> thm -> thm;
193 - providing a list of congruence rules
200 term list -> thm list -> int -> CONSEQ_CONV_direction -> term -> (int * thm option)
203 thm list -> conseq_conv_congruence_syscall ->
212 conseq_conv_congruence list -> (*congruence_list*)
216 (bool * int option * (thm list -> directed_conseq_conv)) list ->
217 (*conversion list:
224 thm list -> (*context that might be used*)
239 context : thm list
240 A list of theorems from the context it may use.
259 new_context : term list
264 old_context : thm list
313 CONSEQ_CONV_context -> conseq_conv_congruence list;
367 conseq_conv_congruence list -> (*congruence_list*)
371 (bool * int option * (thm list -> directed_conseq_conv)) list ->
372 (*conversion list:
378 thm list -> (*context that might be used*)
383 val CONTEXT_DEPTH_CONSEQ_CONV : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> directed_conseq_conv;
384 val CONTEXT_REDEPTH_CONSEQ_CONV : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> directed_conseq_conv;
385 val CONTEXT_ONCE_DEPTH_CONSEQ_CONV : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> directed_conseq_conv;
386 val CONTEXT_NUM_DEPTH_CONSEQ_CONV : CONSEQ_CONV_context -> (thm list -> directed_conseq_conv) -> int ->
388 val CONTEXT_NUM_REDEPTH_CONSEQ_CONV: (thm list -> directed_conseq_conv) -> int ->
402 CONSEQ_REWRITE_CONV. the list of conversions corresponds to the
403 list of directed_conseq_conv for EXT_DEPTH_NUM_CONSEQ_CONV.
408 conseq_conv_congruence list -> (* congruences *)
413 thm list -> (* context *)
414 (bool * int option * (thm list -> conv)) list -> (* conversions *)
415 (thm list * thm list * thm list) -> (*consequence rewrites *)
420 val EXT_CONSEQ_REWRITE_CONV : (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv;
421 val EXT_CONSEQ_HO_REWRITE_CONV : (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv;
422 val EXT_CONTEXT_CONSEQ_REWRITE_CONV : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv;
423 val EXT_CONTEXT_CONSEQ_HO_REWRITE_CONV : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> directed_conseq_conv;
425 val EXT_CONSEQ_REWRITE_TAC : (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic;
426 val EXT_CONTEXT_CONSEQ_REWRITE_TAC : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic;
427 val EXT_CONSEQ_HO_REWRITE_TAC : (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic;
428 val EXT_CONTEXT_CONSEQ_HO_REWRITE_TAC : CONSEQ_CONV_context -> (thm list -> conv) list -> thm list -> (thm list * thm list * thm list) -> tactic;