| /seL4-l4v-master/HOL4/examples/temporal_deep/src/examples/ |
| H A D | ibm.sml | 204 val x1 = if (b1 = 1) then ``P_PROP (7:num)`` else ``P_NOT (P_PROP (7:num))`` value
|
| /seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
| H A D | codegen_inputLib.sml | 94 val x1 = (cdr o car) tm value
|
| H A D | compilerLib.sml | 289 val (x1,x2,x3) = compile target tm value
|
| H A D | codegenLib.sml | 86 val (x1,x2) = split_at (fn c => c = #"/") (explode x) [] value
|
| H A D | reg_allocLib.sml | 320 val (x1,x2) = dest_eq tm value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/x64_compiler/ |
| H A D | x64_codegen_inputLib.sml | 90 val x1 = (cdr o car) tm value
|
| H A D | x64_codegenLib.sml | 44 val (x1,x2) = split_at (fn c => c = #"/") (explode x) [] value
|
| /seL4-l4v-master/HOL4/examples/bootstrap/ |
| H A D | source_propertiesScript.sml | 312 val (x1,y1,z1) = split_at P xs value
|
| H A D | automationLib.sml | 32 val (x1,y1,z1) = split_at P xs value
222 val (x1,x2) = combinSyntax.dest_update up value
|
| /seL4-l4v-master/HOL4/src/TeX/ |
| H A D | holindexData.sml | 338 val (x1,x2) = Substring.splitl (fn c => not (c = #".")) ss2 value
|
| H A D | holindex.sml | 180 val (x1,x2) = Substring.splitl (fn c => not (c = #".")) ss2 value
|
| /seL4-l4v-master/seL4/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/ |
| H A D | types.h | 25 seL4_Word pc, sp, spsr, x0, x1, x2, x3, x4, x5, x6, x7, x8, x16, x17, x18, x29, x30; member in struct:seL4_UserContext_
|
| /seL4-l4v-master/HOL4/examples/dev/sw2/ |
| H A D | refine.sml | 184 let val (x1,x2) = dest_pair x value
|
| /seL4-l4v-master/HOL4/examples/machine-code/graph/ |
| H A D | exportLib.sml | 146 val x1 = tm |> rator |> rand |> stringSyntax.fromHOLstring value
|
| /seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | prog_x64Lib.sml | 273 val x1 = (cdr o cdr o car) tag value
292 val (x1,x2) = dest_comb x12 value
[all...] |
| H A D | prog_x64_extraScript.sml | 168 val x1 = ("r1",``1w:word4``,``r1:word64``) value
|
| H A D | x64_decoderScript.sml | 638 val (x1,x2) = dest_DTF tm value
[all...] |
| /seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_bytecode_stepScript.sml | 107 val (x1,s1) = pred_setSyntax.dest_insert tm value
[all...] |
| /seL4-l4v-master/HOL4/examples/machine-code/multiword/x64/ |
| H A D | x64_multiwordScript.sml | 105 val x1 = ("r1",``1w:word4``,``r1:word64``); value
[all...] |
| /seL4-l4v-master/HOL4/examples/separationLogic/src/ |
| H A D | separationLogicLib.sml | 515 val (x1,x2) = pairSyntax.dest_pair x; value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
| H A D | core_decompilerLib.sml | 498 val x1 = pairSyntax.mk_fst lhs value
[all...] |
| /seL4-l4v-master/HOL4/polyml/libpolyml/ |
| H A D | realconv.cpp | 1043 ULong *x, *x1, *xe, z; variable
1763 ULong *x, *x1, *xe, y; variable
1797 ULong *x, *x0, x1, x2; variable
[all...] |
| /seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
| H A D | lisp_extractLib.sml | 185 val (x1,x2,x3) = dest_cond tm value
692 val x1 value
882 val x1 = pairSyntax.mk_pair(strs,body) value
883 val x1 = pairSyntax.mk_pair(fromMLstring name,x1) value
[all...] |
| /seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/ |
| H A D | milawa_logicScript.sml | 249 val x1 = ``mVar "X1"`` value
[all...] |
| /seL4-l4v-master/HOL4/src/coretypes/ |
| H A D | PairRules.sml | 177 then let val (x1,x2) = dest_pair x value
1628 val (x1,x2) = dest_pair x value
[all...] |