/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | SmtLib_Theories.sml | 142 ("select", K_zero_two Term.mk_comb),
|
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/ |
H A D | tttSyntEval.sml | 199 val _ = msg_synt tml "terms to select from"
|
H A D | tttSearch.sml | 563 (* sort and select node with best selection score *)
|
/seL4-l4v-10.1.1/HOL4/tools-poly/poly/ |
H A D | Help.sml | 223 (* Let the user select from the menu: *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
H A D | reg_allocLib.sml | 381 val w = first (K true) ws (* select most busy *) 402 (* spilling: select a vertex and spill it *) let 406 val w = if ws = [] then fail () else hd ws (* select least busy *)
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | solver.py | 267 'TokenWordsAccess': 'select', 'TokenWordsUpdate': 'store' 572 (concat (concat (select m (bvadd p #x00000003)) (select m (bvadd p #x00000002))) 573 (concat (select m (bvadd p #x00000001)) (select m p)))) 592 (select m p))''', 597 (not (= (select d p) #b0)))''', 610 (select m ((_ extract 31 2) p)))''', 636 (not (= (select d p) #b0)))''', 1191 import select namespace [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | MATCH_COMPILER.sml | 784 val select = PattCodeTupleSelect{tupleNo = thisTuple, fieldOffset = bestcol, next = code } value 786 { leafSet = leafSet, leafCount = leafCount, vars = [], code = select } 1048 select the field. *)
|
/seL4-l4v-10.1.1/HOL4/examples/Crypto/Serpent/Reference/ |
H A D | Serpent_Reference_TransformationScript.sml | 560 (* compute the parity on select bits *)
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Vector.sml | 45 changing that. It's also used in the interface to the RTS in OS.Poll and Socket.select. *)
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | MESSAGE.signature.sml | 862 | LB_SETSEL of { select: bool, index: int } 906 | LB_SELITEMRANGE of { select: bool, first: int, last: int }
|
H A D | Message.sml | 1666 | LB_SETSEL of { select: bool, index: int } 1710 | LB_SELITEMRANGE of { select: bool, first: int, last: int } 2379 | decompileMessage (0x0185, wp, lp) = LB_SETSEL {select = wp <> 0w0, index = SysWord.toInt lp} 2423 | decompileMessage (0x019B, wp, lp) = LB_SELITEMRANGE {select = wp <> 0w0, first = loWord lp, last = hiWord lp} 3137 | compileMessage (LB_SETSEL{select, index}) = (0x0185, SysWord.fromInt(btoi select), SysWord.fromInt index, noFree) 3181 | compileMessage (LB_SELITEMRANGE{select, first, last}) = 3182 (0x019B, SysWord.fromInt(btoi select), makeLong(first, last), noFree)
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Solver.C | 713 Var next = order.select(params.random_var_freq);
|
/seL4-l4v-10.1.1/HOL4/src/basicProof/ |
H A D | BasicProvers.sml | 219 (* select the induction theorem to use. There are 3 kinds of induction *) 237 | SOME thm => (* now select induction tactic *)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/ |
H A D | server.scala | 361 db.using_statement(Data.table.select())(stmt =>
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
H A D | server.scala | 361 db.using_statement(Data.table.select())(stmt =>
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_SIMPLIFIER.sml | 1498 fun select(n, hd::tl) = function 1501 else if BoolVector.sub(filter, n) then hd :: select(n+1, tl) else select(n+1, tl) 1502 | select(_, []) = [] 1503 val selected = select(0, fields)
|
H A D | CODETREE_OPTIMISER.sml | 235 fun buildFullTuple(filter, select) = 240 then select u :: extArg(t+1, u+1)
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/ |
H A D | variableScript.sml | 388 (* The next three corollaries select each property. *)
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/ |
H A D | variableScript.sml | 394 (* The next three corollaries select each property. *)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/ |
H A D | emit_eval.sml | 275 | armML.DataProcessing (armML.Select_Bytes _) => "select bytes"
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | normalForms.sml | 938 val _ = same_const select a orelse raise ERR "norm" "not a select"
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | regAllocation.sml | 387 (* Add a low degree node into the select stack *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | regAllocation.sml | 387 (* Add a low degree node into the select stack *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | regAllocation.sml | 387 (* Add a low degree node into the select stack *)
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Tactic.sml | 1026 * eliminates a select term from the goal. *
|