1(* =====================================================================*) 2(* FILE : cond_rewr.sig *) 3(* DESCRIPTION : Signature for conditional rewriting conversions and *) 4(* tactics *) 5(* AUTHOR : P Curzon *) 6(* DATE : May 1993 *) 7(* =====================================================================*) 8 9signature Cond_rewrite = 10sig 11 12 include Abbrev 13 14 val COND_REWR_TAC 15 :(term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list) 16 -> thm_tactic 17 18 val search_top_down 19 :term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list 20 val COND_REWR_CONV 21 :(term -> term -> ((term,term)subst * (hol_type,hol_type)subst) list) 22 -> thm -> conv 23 val COND_REWR_CANON : thm -> thm 24 val COND_REWRITE1_TAC : thm_tactic 25 val COND_REWRITE1_CONV : thm list -> thm -> conv 26 27end 28