Searched defs:inline (Results 1 - 3 of 3) sorted by last modified time

/seL4-l4v-master/HOL4/examples/dev/sw2/
H A Dinline.sml1 structure inline :> inline = structure
H A Dinline.sig1 signature inline = signature
/seL4-l4v-master/HOL4/examples/dev/
H A DinlineCompile.sml240 fun inline th = let val tm = (snd o dest_eq o snd o dest_thm) th function

Completed in 44 milliseconds