Lines Matching refs:rule
8 val ALL_HYP_CONV_RULE: conv -> rule
9 val ALL_HYP_RULE: rule -> rule
13 val ELIM_UNDISCH: rule
16 val HYP_CANON_RULE: rule
17 val HYP_CONV_RULE: conv -> term -> rule
18 val HYP_RULE: (thm -> thm) -> term -> rule
21 val INST_REWRITE_RULE: thm list -> rule
22 val LIST_DISCH: term list -> rule
23 val MATCH_HYP_CONV_RULE: conv -> term -> rule
24 val MATCH_HYP_RULE: rule -> term -> rule
27 val PRED_HYP_CONV_RULE: conv -> (term -> bool) -> rule
28 val PRED_HYP_RULE: rule -> (term -> bool) -> rule
33 val SET_RULE: rule
35 val SRW_RULE: thm list -> rule
39 val STRIP_UNDISCH: rule
77 val o_RULE: rule