Lines Matching refs:rule
201 type rule = thm -> thm
294 val THENR : rule * rule -> rule
295 val REPEATR : rule -> rule
296 val ORELSER : rule * rule -> rule
297 val TRYR : rule -> rule
298 val ALL_RULE : rule
299 val EVERYR : rule list -> rule
300 val FORALL_IMP : rule
301 val EQ_BOOL_INTRO : rule
302 val GENVAR_BVARS : rule
303 val GENVAR_SPEC : rule
304 val GENVAR_SPEC_ALL : rule
306 val REORDER_ASMS : term list -> rule
307 val NEW_CONST_RULE : term -> rule
308 val GENVAR_CONST_RULE : rule
309 val ZAP_CONSTS_RULE : rule
321 val DISCH_CONJ : term -> rule
322 val DISCH_CONJUNCTS : term list -> rule
323 val DISCH_CONJUNCTS_ALL : rule
324 val DISCH_CONJUNCTS_FILTER : (term -> bool) -> rule
328 val UNDISCH_CONJ : rule
329 val UNDISCH_CONJUNCTS : rule
354 val CNF_RULE : rule