TFL/rules.sig
changeset 3405 2cccd0e3e9ea
parent 3379 7091ffa99c93
child 6498 1ebbe18fe236
equal deleted inserted replaced
3404:91a91790899a 3405:2cccd0e3e9ea
    44 
    44 
    45   val EVEN_ORS : thm list -> thm list
    45   val EVEN_ORS : thm list -> thm list
    46   val DISJ_CASESL : thm -> thm list -> thm
    46   val DISJ_CASESL : thm -> thm list -> thm
    47 
    47 
    48   val SUBS : thm list -> thm -> thm
    48   val SUBS : thm list -> thm -> thm
    49   val simplify : thm list -> thm -> thm
    49   val simpl_conv : simpset -> thm list -> cterm -> thm
    50   val simpl_conv : thm list -> cterm -> thm
       
    51 
    50 
    52 (* For debugging my isabelle solver in the conditional rewriter *)
    51 (* For debugging my isabelle solver in the conditional rewriter *)
    53   val term_ref : term list ref
    52   val term_ref : term list ref
    54   val thm_ref : thm list ref
    53   val thm_ref : thm list ref
    55   val mss_ref : meta_simpset list ref
    54   val mss_ref : meta_simpset list ref
    56   val tracing :bool ref
    55   val tracing :bool ref
    57   val CONTEXT_REWRITE_RULE : term * term
    56   val CONTEXT_REWRITE_RULE : simpset * term * term * thm * thm list 
    58                              -> {cut_lemma:thm, congs: thm list, th:thm} 
    57                              -> thm -> thm * term list
    59                              -> thm * term list
       
    60   val RIGHT_ASSOC : thm -> thm 
    58   val RIGHT_ASSOC : thm -> thm 
    61 
    59 
    62   val prove : cterm * tactic -> thm
    60   val prove : cterm * tactic -> thm
    63 end;
    61 end;