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