Searched defs:pf (Results 1 - 3 of 3) sorted by path

/seL4-l4v-10.1.1/HOL4/src/1/
H A DMutual.sml372 val pf = ((EQ_MP ts_thm) o (MP beta) o LIST_CONJ) value
H A DPrim_rec.sml661 val pf = ((MP beta) o LIST_CONJ) o mapshape(map length gll)pl value
/seL4-l4v-10.1.1/HOL4/src/unwind/
H A DunwindLib.sml368 val pf = (op @) o (pf1##pf2) o CONJ_PAIR value
376 let val (pf,fnn,eqns) = trav p tm [] value

Completed in 91 milliseconds