Searched defs:vc (Results 1 - 8 of 8) sorted by relevance
| /seL4-l4v-master/HOL4/src/HolSat/ |
| H A D | def_cnf.sml | 256 val vc = (n + 1) value
|
| /seL4-l4v-master/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsTools.sml | 342 fun vc vL t = function
|
| /seL4-l4v-master/HOL4/examples/AI_tasks/ |
| H A D | mleCombinLib.sml | 320 val vc = mk_var ("Vc",alpha) value
|
| /seL4-l4v-master/HOL4/src/integer/ |
| H A D | CooperShell.sml | 426 val vc = Arbint.min(Binarymap.find(final_map, v)) value
|
| /seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfoot_pp_print.sml | 904 val (vc, b) = pairSyntax.dest_pabs (el 2 args); value
|
| H A D | holfootLib.sml | 1250 val vc = pairSyntax.mk_pair (v, c_t); value
1541 val vc = pairSyntax.mk_pair (v, c); value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
| H A D | Import.sml | 234 val vc = mk_local_const (f, typ) value
|
| /seL4-l4v-master/HOL4/examples/separationLogic/src/ |
| H A D | vars_as_resourceFunctor.sml | 255 val (vc, thm0) = COND_PROP___STRONG_EXISTS_NORMALISE_CONV___internally false tt value
889 val (vc, _) = dest_COND_PROP___STRONG_EXISTS pre value
909 val (vc, _) = dest_COND_PROP___STRONG_EXISTS post value
1532 val (vc, inv_body_t) = pairSyntax.dest_pabs inv_t value
1637 val (vc, value
1839 val (vc, _) = pairSyntax.dest_pabs P'; value
1950 val vc = pairSyntax.mk_pair (v, c); value
2113 val vc = fst (pairSyntax.dest_pabs pre) value
2401 val (vc, _) = pairSyntax.dest_pabs P'; value
[all...] |
Completed in 102 milliseconds