Searched refs:res0 (Results 1 - 9 of 9) sorted by relevance

/seL4-l4v-master/HOL4/src/opentheory/compat/
H A DHOL4combinScript.sml11 val res0 = export(``I = S K (K:'a->'a->'a)``, value
H A DHOL4boolScript.sml11 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 Dseqmonad.sml9 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 Dgic_v3.h81 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 DHoldep.sml135 val (targetname, res0) = beginentry objext (manglefilename filename)
139 res0
/seL4-l4v-master/HOL4/src/metis/
H A DfolMapping.sml751 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 DPreterm.sml307 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 DCooperCore.sml1118 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 DPrim_rec.sml1920 val res0 = EQT_ELIM (PURE_REWRITE_CONV [body_th,case_def] t) value
1927 List.foldr foldthis (body,res0) vs

Completed in 96 milliseconds