TFL/rules.sig
changeset 3379 7091ffa99c93
parent 3353 9112a2efb9a3
child 3405 2cccd0e3e9ea
equal deleted inserted replaced
3378:11f4884a071a 3379:7091ffa99c93
    48   val SUBS : thm list -> thm -> thm
    48   val SUBS : thm list -> thm -> thm
    49   val simplify : thm list -> thm -> thm
    49   val simplify : thm list -> thm -> thm
    50   val simpl_conv : thm list -> cterm -> thm
    50   val simpl_conv : thm list -> cterm -> thm
    51 
    51 
    52 (* For debugging my isabelle solver in the conditional rewriter *)
    52 (* For debugging my isabelle solver in the conditional rewriter *)
    53 (*
       
    54   val term_ref : term list ref
    53   val term_ref : term list ref
    55   val thm_ref : thm list ref
    54   val thm_ref : thm list ref
    56   val mss_ref : meta_simpset list ref
    55   val mss_ref : meta_simpset list ref
    57   val tracing :bool ref
    56   val tracing :bool ref
    58 *)
       
    59   val CONTEXT_REWRITE_RULE : term * term
    57   val CONTEXT_REWRITE_RULE : term * term
    60                              -> {thms:thm list,congs: thm list, th:thm} 
    58                              -> {cut_lemma:thm, congs: thm list, th:thm} 
    61                              -> thm * term list
    59                              -> thm * term list
    62   val RIGHT_ASSOC : thm -> thm 
    60   val RIGHT_ASSOC : thm -> thm 
    63 
    61 
    64   val prove : cterm * tactic -> thm
    62   val prove : cterm * tactic -> thm
    65 end;
    63 end;