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