Lines Matching refs:rule
21 val RW : thm list -> rule
22 val RW1 : thm list -> rule
91 val BASIC_SEP_REWRITE_RULE : thm -> rule
92 val EXISTS_PRE : term frag list -> rule
93 val EXISTS_SEP_REWRITE_RULE : thm -> rule
94 val HIDE_POST_RULE : term -> rule
95 val HIDE_PRE_RULE : term -> rule
96 val HIDE_PRE_STATUS_RULE : thm -> rule
97 val HIDE_STATUS_RULE : bool -> thm -> rule
98 val INST_SPEC : thm -> rule
99 val LIST_HIDE_POST_RULE : term list -> rule
100 val MERGE_CONDS_RULE : rule
101 val MOVE_COND_RULE : term -> rule
102 val PRE_POST_RULE : conv -> rule
103 val SEP_EXISTS_ELIM_RULE : rule
104 val SEP_EXISTS_POST_RULE : term -> rule
105 val SEP_EXISTS_PRE_RULE : term -> rule
106 val SEP_REWRITE_RULE : thm list -> rule
107 val SUBST_INST : {redex: term, residue: term} list -> rule
108 val UNHIDE_PRE_RULE : term -> rule
110 val HIDE_SEP_IMP_POST_RULE : term -> rule
111 val LIST_HIDE_SEP_IMP_POST_RULE : term list -> rule
118 val SPECC_FRAME_RULE : term -> rule
119 val SPECL_FRAME_RULE : term list -> rule
121 val SPEC_SORT_CODE_RULE : rule