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

/seL4-l4v-10.1.1/HOL4/src/pfl/
H A Dindex.sml398 fun patch pat plist = map (fn (ctxt,e) => (mk_eq(ob,pat)::ctxt,e)) plist function
405 fun patch (x,M) (ctxt,e) = (mk_eq(x,M)::ctxt, body) function

Completed in 32 milliseconds