Lines Matching refs:cl
34 fun AXIOM cl =
35 if List.all is_literal cl then mlibThm (cl, (Axiom, []))
44 fun INST env (th as mlibThm (cl, pr)) =
46 val cl' = map (formula_subst env) cl
48 if cl' = cl then th else
50 => if cl' = clause th' then th' else mlibThm (cl', (Inst, [th']))
51 | _ => mlibThm (cl', (Inst, [th]))
55 let val cl = rev (setify (clause th))
56 in if cl = clause th then th else mlibThm (cl, (Factor, [th]))
65 val cl = cl1' @ cl2'
67 if cl = cl1 then th1
68 else if cl = cl2 then th2
69 else mlibThm (cl, (Resolve, [th1, th2]))