| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | realconv.cpp | 1836 Long e, e1; variable
2567 int bb2, bb5, bbe, bd2, bd5, bbbits, bs2, c, e, e1; variable
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/floating-point/native/ |
| H A D | selftest.sml | 98 val e1 = EVAL tm value
149 val e1 = EVAL tm value
186 val e1 = EVAL tm value
|
| /seL4-l4v-10.1.1/HOL4/src/floating-point/ |
| H A D | binary_ieeeLib.sml | 390 val e1 = boolSyntax.mk_neg e0 value
|
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolScript.sml | 1575 val e1 = CHOOSE (x,ASSUME ep) th1 and e2 = CHOOSE (x,ASSUME eq) th2 value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/bag/ |
| H A D | bagSimpleLib.sml | 51 val (e1,b') = bagSyntax.dest_insert b; value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Conv.sml | 804 val e1 = CHOOSE (x, ASSUME disj1) (eotm t1) value
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootLib.sml | 1284 val (e1, tag_t, e2) = dest_holfoot_prog_field_assign p1 value
1331 val (e1, tag_t, e2) = dest_holfoot_prog_field_assign p1 value
1648 val (e1,_) = dest_holfoot_ap_points_to ttt value
1749 val (e1,_) = dest_holfoot_ap_points_to ttt value
1982 val (e1,_) = dest_holfoot_ap_points_to ttt value
2028 val (e1, ttt, has_data, n, m) = valOf found_opt; value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
| H A D | regAlloc.sml | [all...] |
| H A D | refine.sml | [all...] |
| H A D | NormalScript.sml | 302 ``(let f = fun e1 in e2 f) = e2 e1``, function
315 ``(let v = atom v in let f = fun (e1 v) in e2 f) = function
332 ``(let f = fun e1 in e2 f) = e2 e1``, function
339 ``(\\x. let f = fun e1 in e2 f) = (let f = fun e1 in (\\x. e2 f))``, function
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | IR.sml | [all...] |
| /seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/ |
| H A D | decidable_separationLogicLib.sml | 290 val (e1, e2) = dest_pf_unequal pf; value
299 val (e1, e2) = dest_pf_equal pf; value
307 val (e1, e2) = dest_pf_unequal pf; value
370 val (e1, e2) = dest_pf_equal pf1; value
378 val (e1, e2) = dest_pf_unequal pf1; value
576 val (e1, e2) = pairLib.dest_pair t; value
809 val (e1, e2) = dest_pf_equal pf; value
821 val (e1, e2) = dest_pf_equal uneq; value
877 val (e1, e2) = dest_pf_unequal h; value
878 val (e1, turn) = if is_dse_nil e2 then (e1, true) else value
891 val (e1, e2) = dest_pf_unequal h; value
1013 val (e1, _, a1, aL1) = dest_sf_points_to sf1; value
1031 val (e1, a1, _, _) = dest_sf_points_to sf1; value
1242 val (e1, _, _, _) = dest_sf_points_to sf; value
1630 val e1 = snd (first (fn (x,y) => x = f1) pointer_list); value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | lzConv.sml | 733 val e1 = CHOOSE (x,ASSUME disj1) (eotm t1) value
|