1139749Simpsignature Rewrite = 2230132Suqssig 321769Sjkh include Abbrev 421769Sjkh type rewrites 521769Sjkh 621769Sjkh val empty_rewrites : rewrites 721769Sjkh val mk_rewrites : thm -> thm list 821769Sjkh val add_rewrites : rewrites -> thm list -> rewrites 921769Sjkh val dest_rewrites : rewrites -> thm list 1021769Sjkh val net_of : rewrites -> conv Net.net 1121769Sjkh 1221769Sjkh val implicit_rewrites : unit -> rewrites 1321769Sjkh val set_implicit_rewrites : rewrites -> unit 1421769Sjkh val add_implicit_rewrites : thm list -> unit 1521769Sjkh 1621769Sjkh val pp_rewrites : rewrites Parse.pprinter 1721769Sjkh val bool_rewrites : rewrites 1821769Sjkh val monitoring : bool ref 1921769Sjkh 2021769Sjkh val REWRITES_CONV : rewrites -> conv 2121769Sjkh val GEN_REWRITE_CONV : (conv -> conv) -> rewrites -> thm list -> conv 2221769Sjkh val GEN_REWRITE_RULE : (conv -> conv) -> rewrites -> thm list -> thm -> thm 2321769Sjkh val GEN_REWRITE_TAC : (conv -> conv) -> rewrites -> thm list -> tactic 2421769Sjkh 2521769Sjkh val REWRITE_CONV : thm list -> conv 2629877Smsmith val PURE_REWRITE_CONV : thm list -> conv 2752286Smdodd val ONCE_REWRITE_CONV : thm list -> conv 2852286Smdodd val PURE_ONCE_REWRITE_CONV : thm list -> conv 2952286Smdodd 3021769Sjkh val PURE_REWRITE_RULE : thm list -> thm -> thm 3121769Sjkh val REWRITE_RULE : thm list -> thm -> thm 32119418Sobrien val PURE_ONCE_REWRITE_RULE : thm list -> thm -> thm 33119418Sobrien val ONCE_REWRITE_RULE : thm list -> thm -> thm 34119418Sobrien val PURE_ASM_REWRITE_RULE : thm list -> thm -> thm 3521769Sjkh val ASM_REWRITE_RULE : thm list -> thm -> thm 3629877Smsmith val PURE_ONCE_ASM_REWRITE_RULE: thm list -> thm -> thm 3721769Sjkh val ONCE_ASM_REWRITE_RULE : thm list -> thm -> thm 3821769Sjkh 3921769Sjkh val PURE_REWRITE_TAC : thm list -> tactic 40112731Smdodd val REWRITE_TAC : thm list -> tactic 4121769Sjkh val rewrite_tac : thm list -> tactic 4221769Sjkh val PURE_ONCE_REWRITE_TAC : thm list -> tactic 4321769Sjkh val ONCE_REWRITE_TAC : thm list -> tactic 4421769Sjkh val once_rewrite_tac : thm list -> tactic 4521769Sjkh val PURE_ASM_REWRITE_TAC : thm list -> tactic 4652286Smdodd val ASM_REWRITE_TAC : thm list -> tactic 4724204Sbde val asm_rewrite_tac : thm list -> tactic 4821769Sjkh val PURE_ONCE_ASM_REWRITE_TAC : thm list -> tactic 4921769Sjkh val ONCE_ASM_REWRITE_TAC : thm list -> tactic 5021769Sjkh val once_asm_rewrite_tac : thm list -> tactic 5152286Smdodd 5252286Smdodd type pred = term -> bool 5352286Smdodd 5452286Smdodd val FILTER_PURE_ASM_REWRITE_RULE : pred -> thm list -> thm -> thm 5552286Smdodd val FILTER_ASM_REWRITE_RULE : pred -> thm list -> thm -> thm 5652286Smdodd val FILTER_PURE_ONCE_ASM_REWRITE_RULE : pred -> thm list -> thm -> thm 5752286Smdodd val FILTER_ONCE_ASM_REWRITE_RULE : pred -> thm list -> thm -> thm 5857987Smdodd val FILTER_PURE_ASM_REWRITE_TAC : pred -> thm list -> tactic 59257176Sglebius val FILTER_ASM_REWRITE_TAC : pred -> thm list -> tactic 6057987Smdodd val FILTER_PURE_ONCE_ASM_REWRITE_TAC : pred -> thm list -> tactic 61112731Smdodd val FILTER_ONCE_ASM_REWRITE_TAC : pred -> thm list -> tactic 6257987Smdodd 63147256Sbrooks val SUBST_MATCH : thm -> thm -> thm 6450026Smdodd 6557987Smdoddend 6621769Sjkh