Searched defs:xenv (Results 1 - 2 of 2) sorted by last modified time
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
| H A D | vars_as_resourceFunctor.sml | 330 val (xenv,penv,prog,abst) = dest_ASL_PROGRAM_IS_ABSTRACTION tt value
1086 val (xenv, penv) = let (* a crude, but robust and simple way *) value
1090 val xenv = rand (rator t0) value
[all...] |
| H A D | separationLogicLib.sml | 488 val (xenv, penv, pre, body, post) = dest_ASL_PROGRAM_HOARE_TRIPLE t; value
509 val (xenv, penv, p1, p3) = dest_ASL_PROGRAM_IS_ABSTRACTION t handle HOL_ERR _ => raise UNCHANGED value
[all...] |
Completed in 68 milliseconds