1signature Ho_Rewrite =
2sig
3  include Abbrev
4
5  val mk_rewrites                : thm -> thm list
6
7  val implicit_rewrites          : unit -> thm list
8  val set_implicit_rewrites      : thm list -> unit
9  val add_implicit_rewrites      : thm list -> unit
10
11  val GEN_REWRITE_CONV           : (conv -> conv) -> thm list -> conv
12  val GEN_REWRITE_RULE           : (conv -> conv) -> thm list -> thm -> thm
13  val GEN_REWRITE_TAC            : (conv -> conv) -> thm list -> tactic
14
15  val PURE_REWRITE_CONV          : thm list -> conv
16  val REWRITE_CONV               : thm list -> conv
17  val HIGHER_REWRITE_CONV        : thm list -> conv
18  val PURE_ONCE_REWRITE_CONV     : thm list -> conv
19  val ONCE_REWRITE_CONV          : thm list -> conv
20
21  val PURE_REWRITE_RULE          : thm list -> thm -> thm
22  val REWRITE_RULE               : thm list -> thm -> thm
23  val PURE_ONCE_REWRITE_RULE     : thm list -> thm -> thm
24  val ONCE_REWRITE_RULE          : thm list -> thm -> thm
25  val PURE_ASM_REWRITE_RULE      : thm list -> thm -> thm
26  val ASM_REWRITE_RULE           : thm list -> thm -> thm
27  val PURE_ONCE_ASM_REWRITE_RULE : thm list -> thm -> thm
28  val ONCE_ASM_REWRITE_RULE      : thm list -> thm -> thm
29
30  val PURE_REWRITE_TAC           : thm list -> tactic
31  val REWRITE_TAC                : thm list -> tactic
32  val PURE_ONCE_REWRITE_TAC      : thm list -> tactic
33  val ONCE_REWRITE_TAC           : thm list -> tactic
34  val PURE_ASM_REWRITE_TAC       : thm list -> tactic
35  val ASM_REWRITE_TAC            : thm list -> tactic
36  val PURE_ONCE_ASM_REWRITE_TAC  : thm list -> tactic
37  val ONCE_ASM_REWRITE_TAC       : thm list -> tactic
38
39  type pred = term -> bool
40
41  val FILTER_PURE_ASM_REWRITE_RULE      : pred -> thm list -> thm -> thm
42  val FILTER_ASM_REWRITE_RULE           : pred -> thm list -> thm -> thm
43  val FILTER_PURE_ONCE_ASM_REWRITE_RULE : pred -> thm list -> thm -> thm
44  val FILTER_ONCE_ASM_REWRITE_RULE      : pred -> thm list -> thm -> thm
45  val FILTER_PURE_ASM_REWRITE_TAC       : pred -> thm list -> tactic
46  val FILTER_ASM_REWRITE_TAC            : pred -> thm list -> tactic
47  val FILTER_PURE_ONCE_ASM_REWRITE_TAC  : pred -> thm list -> tactic
48  val FILTER_ONCE_ASM_REWRITE_TAC       : pred -> thm list -> tactic
49
50  val SUBST_MATCH : thm -> thm -> thm
51
52  val REQUIRE0_TAC         : thm -> tactic -> tactic
53  val REQUIRE_DECREASE_TAC : thm -> tactic -> tactic
54
55end
56