Lines Matching refs:list
5 val mk_rewrites : thm -> thm list
7 val implicit_rewrites : unit -> thm list
8 val set_implicit_rewrites : thm list -> unit
9 val add_implicit_rewrites : thm list -> unit
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
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
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
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
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