1157016Sdessignature Ho_Rewrite = 298937Sdessig 3124208Sdes include Abbrev 4124208Sdes 5124208Sdes val mk_rewrites : thm -> thm list 6124208Sdes 7124208Sdes val implicit_rewrites : unit -> thm list 8124208Sdes val set_implicit_rewrites : thm list -> unit 9124208Sdes val add_implicit_rewrites : thm list -> unit 10124208Sdes 11124208Sdes val GEN_REWRITE_CONV : (conv -> conv) -> thm list -> conv 12124208Sdes val GEN_REWRITE_RULE : (conv -> conv) -> thm list -> thm -> thm 13124208Sdes val GEN_REWRITE_TAC : (conv -> conv) -> thm list -> tactic 14124208Sdes 15124208Sdes val PURE_REWRITE_CONV : thm list -> conv 16124208Sdes val REWRITE_CONV : thm list -> conv 17124208Sdes val HIGHER_REWRITE_CONV : thm list -> conv 18124208Sdes val PURE_ONCE_REWRITE_CONV : thm list -> conv 19124208Sdes val ONCE_REWRITE_CONV : thm list -> conv 20124208Sdes 21124208Sdes val PURE_REWRITE_RULE : thm list -> thm -> thm 22124208Sdes val REWRITE_RULE : thm list -> thm -> thm 23124208Sdes val PURE_ONCE_REWRITE_RULE : thm list -> thm -> thm 24124208Sdes val ONCE_REWRITE_RULE : thm list -> thm -> thm 25124208Sdes val PURE_ASM_REWRITE_RULE : thm list -> thm -> thm 26124208Sdes val ASM_REWRITE_RULE : thm list -> thm -> thm 27124208Sdes val PURE_ONCE_ASM_REWRITE_RULE : thm list -> thm -> thm 2898937Sdes val ONCE_ASM_REWRITE_RULE : thm list -> thm -> thm 29124208Sdes 30124208Sdes val PURE_REWRITE_TAC : thm list -> tactic 3198937Sdes val REWRITE_TAC : thm list -> tactic 32124208Sdes val PURE_ONCE_REWRITE_TAC : thm list -> tactic 33124208Sdes val ONCE_REWRITE_TAC : thm list -> tactic 3498937Sdes val PURE_ASM_REWRITE_TAC : thm list -> tactic 3598937Sdes val ASM_REWRITE_TAC : thm list -> tactic 3698937Sdes val PURE_ONCE_ASM_REWRITE_TAC : thm list -> tactic 3798937Sdes val ONCE_ASM_REWRITE_TAC : thm list -> tactic 3898937Sdes 39113908Sdes type pred = term -> bool 40124208Sdes 4198937Sdes val FILTER_PURE_ASM_REWRITE_RULE : pred -> thm list -> thm -> thm 42124208Sdes val FILTER_ASM_REWRITE_RULE : pred -> thm list -> thm -> thm 43124208Sdes val FILTER_PURE_ONCE_ASM_REWRITE_RULE : pred -> thm list -> thm -> thm 44124208Sdes val FILTER_ONCE_ASM_REWRITE_RULE : pred -> thm list -> thm -> thm 45124208Sdes val FILTER_PURE_ASM_REWRITE_TAC : pred -> thm list -> tactic 46124208Sdes val FILTER_ASM_REWRITE_TAC : pred -> thm list -> tactic 47124208Sdes val FILTER_PURE_ONCE_ASM_REWRITE_TAC : pred -> thm list -> tactic 48124208Sdes val FILTER_ONCE_ASM_REWRITE_TAC : pred -> thm list -> tactic 49124208Sdes 50124208Sdes val SUBST_MATCH : thm -> thm -> thm 51137015Sdes 52137015Sdes val REQUIRE0_TAC : thm -> tactic -> tactic 53137015Sdes val REQUIRE_DECREASE_TAC : thm -> tactic -> tactic 54137015Sdes 55124208Sdesend 56124208Sdes