TFL/rules.sig
changeset 3379 7091ffa99c93
parent 3353 9112a2efb9a3
child 3405 2cccd0e3e9ea
     1.1 --- a/TFL/rules.sig	Fri May 30 15:30:52 1997 +0200
     1.2 +++ b/TFL/rules.sig	Fri May 30 15:55:27 1997 +0200
     1.3 @@ -50,14 +50,12 @@
     1.4    val simpl_conv : thm list -> cterm -> thm
     1.5  
     1.6  (* For debugging my isabelle solver in the conditional rewriter *)
     1.7 -(*
     1.8    val term_ref : term list ref
     1.9    val thm_ref : thm list ref
    1.10    val mss_ref : meta_simpset list ref
    1.11    val tracing :bool ref
    1.12 -*)
    1.13    val CONTEXT_REWRITE_RULE : term * term
    1.14 -                             -> {thms:thm list,congs: thm list, th:thm} 
    1.15 +                             -> {cut_lemma:thm, congs: thm list, th:thm} 
    1.16                               -> thm * term list
    1.17    val RIGHT_ASSOC : thm -> thm 
    1.18