Searched defs:t4 (Results 1 - 8 of 8) sorted by relevance
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | funcCall.sml | 139 val t4 = regAlloc.parallel_move src0 src t3 value
|
H A D | Normal.sml | 421 val t4 = rhs (concl (GEN_ALL lem3)) (* SPEC_ALL? *) value
|
/seL4-l4v-master/seL4/libsel4/arch_include/riscv/sel4/arch/ |
H A D | types.h | 60 seL4_Word t4; member in struct:seL4_UserContext_
|
/seL4-l4v-master/seL4/include/arch/riscv/arch/machine/ |
H A D | registerset.h | 60 t4 = 28, enumerator in enum:_register
|
/seL4-l4v-master/HOL4/src/datatype/ |
H A D | DatatypeSimps.sml | 173 val t4 = list_mk_forall (args, t3) value 183 val t4 = list_mk_forall ([input_arg, input_arg']@(List.map snd case_args)@(List.map snd case_args'), t3) value 216 val t4 = list_mk_forall ([input_arg, const]@consts, t3) value 251 val t4 = mk_eq (t3a, t3b) value 288 val t4 = list_mk_forall ([input_arg, const]@consts, t3) value [all...] |
/seL4-l4v-master/HOL4/src/pattern_matches/ |
H A D | constrFamiliesLib.sml | 429 val t4 = SOME (mk_case_const_cong_thm_term case_const constrL) value
|
/seL4-l4v-master/HOL4/src/floating-point/ |
H A D | binary_ieeeScript.sml | 1879 val t4 = value
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | mechReasoning.sml | 722 val t4 = Term `?r'' m''. ^t3 = (r'', m'')` value
|
Completed in 147 milliseconds