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