Searched defs:ex (Results 1 - 17 of 17) sorted by relevance
| /seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
| H A D | QbfCertificate.sml | 339 val ex = EXISTS (mk_exists(v,mk_eq(v,w)),w) (REFL w) value
343 val ex = EXISTS (mk_exists(v,mk_eq(v,w)),w) (REFL w) value
|
| /seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
| H A D | Witness.sml | 173 val ex = mk_exists(var, tm') value
|
| /seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
| H A D | swapScript.sml | 642 val ex = (UNDISCH o value
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/ |
| H A D | CoIndDefLib.sml | 42 val ex = foldl ex_fn (ASSUME conj) (rev vars) value
83 val (ex, th1') = intro_exists_left th1 value
|
| H A D | IndDefRules.sml | 542 val ex = mk_exists(v,pat) value
|
| /seL4-l4v-10.1.1/HOL4/src/res_quan/src/ |
| H A D | res_quanLib.sml | 575 val ex = list_mk_abs((tl leftvars), rh) value
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibModel.sml | 523 fun ex v x = map (fn n => insertv (x |-> n) v) (interval 0 (msize m)) function
|
| H A D | normalForms.sml | 969 val ex = mk_exists (v, body) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_opsScript.sml | 86 fun ex tm = let function
|
| H A D | lisp_parseScript.sml | 3101 fun ex tm = let function
|
| /seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/ |
| H A D | decidable_separationLogicLib.sml | 694 val (ex, a, _, _) = dest_sf_points_to h; value
1257 val ex = get_points_to_list_cond_exp sf; value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/quotient/examples/ |
| H A D | ind_rel.sml | 1222 val ex = mk_exists(v,pat) value
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_opsScript.sml | 135 fun ex tm = let function
[all...] |
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
| H A D | CODEGEN_PARSETREE.sml | 952 val ex = exval; value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Drule.sml | 2293 val ex = mk_exists (a, sra) value
2342 val ex = value
|
| H A D | Prim_rec.sml | |
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolScript.sml | 3262 val ex = ���?x. ^P x��� value
|
Completed in 233 milliseconds