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