Lines Matching defs:form
60 (* Counting the clauses that would be generated by conjunctive normal form. *)
644 fun form fm =
649 | And (_,_,s) => Formula.listMkConj (Set.transform form s)
650 | Or (_,_,s) => Formula.listMkDisj (Set.transform form s)
655 Formula.listMkEquiv (Set.transform form s)
657 | Exists (_,_,n,f) => Formula.listMkExists (NameSet.toList n, form f)
658 | Forall (_,_,n,f) => Formula.listMkForall (NameSet.toList n, form f);
660 val toFormula = form;
679 (* Negation normal form. *)
685 (* Basic conjunctive normal form. *)
899 (* Conjunctive normal form derivations. *)
1272 (* Definitional conjunctive normal form. *)