Searched defs:cnf (Results 1 - 9 of 9) sorted by relevance

/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DNormalize.sig45 type cnf type
53 val cnf : Formula.formula -> Thm.clause list value
H A Dselftest.sml517 val cnf = pvFm o clausesToFormula o Normalize.cnf o value
[all...]
H A DNormalize.sml1275 datatype cnf = type
1381 fun cnf fm = function
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DNormalize.sig45 type cnf type
53 val cnf : Formula.formula -> Thm.clause list value
H A Dselftest.sml517 val cnf = pvFm o clausesToFormula o Normalize.cnf o value
[all...]
H A DNormalize.sml1275 datatype cnf = type
1381 fun cnf fm = function
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibCanon.sig32 val cnf : formula -> formula (* simp + nnf + skolemize + purecnf *) value
H A DmlibCanon.sml204 val cnf = list_mk_conj o map list_mk_disj o clausal; value
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DcearTools.sml594 val cnf = f value

Completed in 119 milliseconds