Lines Matching refs:rule
204 type rule = thm -> thm
298 val THENR : rule * rule -> rule
299 val REPEATR : rule -> rule
300 val ORELSER : rule * rule -> rule
301 val TRYR : rule -> rule
302 val ALL_RULE : rule
303 val EVERYR : rule list -> rule
304 val FORALL_IMP : rule
305 val EQ_BOOL_INTRO : rule
306 val GENVAR_BVARS : rule
307 val GENVAR_SPEC : rule
308 val GENVAR_SPEC_ALL : rule
310 val REORDER_ASMS : term list -> rule
311 val NEW_CONST_RULE : term -> rule
312 val GENVAR_CONST_RULE : rule
313 val ZAP_CONSTS_RULE : rule
325 val DISCH_CONJ : term -> rule
326 val DISCH_CONJUNCTS : term list -> rule
327 val DISCH_CONJUNCTS_ALL : rule
328 val DISCH_CONJUNCTS_FILTER : (term -> bool) -> rule
332 val UNDISCH_CONJ : rule
333 val UNDISCH_CONJUNCTS : rule
358 val CNF_RULE : rule