Searched refs:res0 (Results 1 - 9 of 9) sorted by relevance
/seL4-l4v-master/HOL4/src/opentheory/compat/ |
H A D | HOL4combinScript.sml | 11 val res0 = export(``I = S K (K:'a->'a->'a)``, value
|
H A D | HOL4boolScript.sml | 11 val res0 = export(``!t. F ==> t``, value 61 |> C MP (DISCH_ALL(SYM(UNDISCH(MATCH_MP res8 (SPEC_ALL res0)))))
|
/seL4-l4v-master/HOL4/src/portableML/monads/ |
H A D | seqmonad.sml | 9 seq.delay (fn () => let val res0 = m1 env value 11 seq.flatten (seq.map (fn (e, v) => f v e) res0)
|
/seL4-l4v-master/seL4/include/arch/arm/arch/machine/ |
H A D | gic_v3.h | 81 uint32_t res0; /* 0x000C */ member in struct:gic_dist_map 126 uint32_t res0[10]; /* 0x0018 */ member in struct:gic_rdist_map 142 uint32_t res0[32]; /* 0x0000 */ member in struct:gic_rdist_sgi_ppi_map
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holdep.sml | 135 val (targetname, res0) = beginentry objext (manglefilename filename) 139 res0
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | folMapping.sml | 751 fun res0 fth fl = function 762 val ((hol_ms1, hol_lits1), hol_th1) = res0 fol_th1 fol_lit 763 val ((hol_ms2, hol_lits2), hol_th2) = res0 fol_th2 (negate fol_lit)
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Preterm.sml | 307 val res0 = funpow (length inst) (#2 o dest_abs) f_t value 309 list_mk_comb(Term.subst inst res0,
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | CooperCore.sml | 1118 val res0 = CHOOSE (k, exists_small_k) disj1_or_disj2 value 1119 val res1 = CHOOSE (u, little_c_ex) res0
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | Prim_rec.sml | 1920 val res0 = EQT_ELIM (PURE_REWRITE_CONV [body_th,case_def] t) value 1927 List.foldr foldthis (body,res0) vs
|
Completed in 96 milliseconds