src/1/ConseqConv.sig

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;