Lines Matching defs:conj
314 (* proves a conjunction 'conj', provided each conjunct is proved
316 fun prove_conj dict conj =
317 Redblackmap.find (dict, conj)
320 val (l, r) = boolSyntax.dest_conj conj
540 val conj = boolSyntax.dest_neg lhs
541 (* conj |- rhs *)
542 val thm = Library.conj_elim (Thm.ASSUME conj, rhs) (* may fail *)
545 (state, Drule.IMP_ELIM (Thm.DISCH conj thm))
763 profile "rewrite(04)(conj/disj)" (fn () =>
765 (state, profile "rewrite(04.1)(conj)" rewrite_conj (l, r))