1signature Rewrite =
2sig
3  include Abbrev
4  type rewrites
5
6  val empty_rewrites        : rewrites
7  val mk_rewrites           : thm -> thm list
8  val add_rewrites          : rewrites -> thm list -> rewrites
9  val dest_rewrites         : rewrites -> thm list
10  val net_of                : rewrites -> conv Net.net
11
12  val implicit_rewrites     : unit -> rewrites
13  val set_implicit_rewrites : rewrites -> unit
14  val add_implicit_rewrites : thm list -> unit
15
16  val pp_rewrites           : rewrites Parse.pprinter
17  val bool_rewrites         : rewrites
18  val monitoring            : bool ref
19
20  val REWRITES_CONV         : rewrites -> conv
21  val GEN_REWRITE_CONV : (conv -> conv) -> rewrites -> thm list -> conv
22  val GEN_REWRITE_RULE : (conv -> conv) -> rewrites -> thm list -> thm -> thm
23  val GEN_REWRITE_TAC  : (conv -> conv) -> rewrites -> thm list -> tactic
24
25  val REWRITE_CONV              : thm list -> conv
26  val PURE_REWRITE_CONV         : thm list -> conv
27  val ONCE_REWRITE_CONV         : thm list -> conv
28  val PURE_ONCE_REWRITE_CONV    : thm list -> conv
29
30  val PURE_REWRITE_RULE         : thm list -> thm -> thm
31  val REWRITE_RULE              : thm list -> thm -> thm
32  val PURE_ONCE_REWRITE_RULE    : thm list -> thm -> thm
33  val ONCE_REWRITE_RULE         : thm list -> thm -> thm
34  val PURE_ASM_REWRITE_RULE     : thm list -> thm -> thm
35  val ASM_REWRITE_RULE          : thm list -> thm -> thm
36  val PURE_ONCE_ASM_REWRITE_RULE: thm list -> thm -> thm
37  val ONCE_ASM_REWRITE_RULE     : thm list -> thm -> thm
38
39  val PURE_REWRITE_TAC          : thm list -> tactic
40  val REWRITE_TAC               : thm list -> tactic
41  val rewrite_tac               : thm list -> tactic
42  val PURE_ONCE_REWRITE_TAC     : thm list -> tactic
43  val ONCE_REWRITE_TAC          : thm list -> tactic
44  val once_rewrite_tac          : thm list -> tactic
45  val PURE_ASM_REWRITE_TAC      : thm list -> tactic
46  val ASM_REWRITE_TAC           : thm list -> tactic
47  val asm_rewrite_tac           : thm list -> tactic
48  val PURE_ONCE_ASM_REWRITE_TAC : thm list -> tactic
49  val ONCE_ASM_REWRITE_TAC      : thm list -> tactic
50  val once_asm_rewrite_tac      : thm list -> tactic
51
52  type pred = term -> bool
53
54  val FILTER_PURE_ASM_REWRITE_RULE      : pred -> thm list -> thm -> thm
55  val FILTER_ASM_REWRITE_RULE           : pred -> thm list -> thm -> thm
56  val FILTER_PURE_ONCE_ASM_REWRITE_RULE : pred -> thm list -> thm -> thm
57  val FILTER_ONCE_ASM_REWRITE_RULE      : pred -> thm list -> thm -> thm
58  val FILTER_PURE_ASM_REWRITE_TAC       : pred -> thm list -> tactic
59  val FILTER_ASM_REWRITE_TAC            : pred -> thm list -> tactic
60  val FILTER_PURE_ONCE_ASM_REWRITE_TAC  : pred -> thm list -> tactic
61  val FILTER_ONCE_ASM_REWRITE_TAC       : pred -> thm list -> tactic
62
63  val SUBST_MATCH : thm -> thm -> thm
64
65end
66