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

/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/
H A Dset_sepScript.sml14 val cond_def = Define `cond c = \s. (s = {}) /\ c`; value

Completed in 69 milliseconds