/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | QuantHeuristics.tex | 267 \[\begin{array}{r@{\quad \Longleftrightarrow \quad}l} 273 \end{array}\] 285 \[\begin{array}{r@{\quad \Longleftrightarrow \quad}l} 288 \end{array}\]
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | QuantHeuristics.tex | 257 \[\begin{array}{r@{\quad \Longleftrightarrow \quad}l} 263 \end{array}\] 275 \[\begin{array}{r@{\quad \Longleftrightarrow \quad}l} 278 \end{array}\]
|
H A D | libraries.tex | 105 \begin{array}{lcl} 114 \end{array} 787 \begin{array}{cl} 797 \end{array} 2408 \begin{array}[t]{l} 2413 \end{array} 2416 \begin{array}{l} 2419 \end{array} 2438 \begin{array}{l} 2441 \end{array} [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_STATIC_LINK_AND_CASES.sml | 66 val closuresForLocals = Array.array(localCount, false) 67 val newLocalAddresses = Array.array (localCount, 0) 68 val argProperties = Array.array(localCount, []) 746 val argClosureArray = Array.array(List.length argTypes, TriUnref)
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | Color.sml | 113 (* Copy the elements into the array. *)
|
H A D | Dialog.sml | 361 val basis = Word8Array.array (18, 0w0) 405 val basis = Word8Array.array(18, 0w0)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 90 \[\begin{array}{rcl} 110 \end{array} 643 \[ \begin{array}{c} 647 \end{array}
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 90 \[\begin{array}{rcl} 110 \end{array} 643 \[ \begin{array}{c} 647 \end{array}
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/kernel/ |
H A D | ept.c | 55 asid_map_t asid_map = poolPtr->array[asid & MASK(asidLowBits)]; 58 poolPtr->array[asid & MASK(asidLowBits)] = asid_map_asid_map_none_new();
|
/seL4-l4v-10.1.1/HOL4/Manual/Logic/ |
H A D | syntax.tex | 935 (b\imp b') = \left\{ \begin{array}{ll} 938 \end{array} 947 (x=_{X}x') = \left\{ \begin{array}{ll} 950 \end{array} 959 \ch_{X}(f) = \left\{ \begin{array}{ll} 963 \end{array}
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Logic/ |
H A D | syntax.tex | 943 (b\imp b') = \left\{ \begin{array}{ll} 946 \end{array} 955 (x=_{X}x') = \left\{ \begin{array}{ll} 958 \end{array} 967 \ch_{X}(f) = \left\{ \begin{array}{ll} 971 \end{array}
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/prog/ |
H A D | arm8_progLib.sml | 473 ["array-mem32", "mem-array32", "array32"], 474 ["array-mem64", "mem-array64", "array64"],
|
/seL4-l4v-10.1.1/HOL4/src/Boolify/test/ |
H A D | datatypes.sml | 174 `array = Arry of num => 'A list`; 181 | Array of value array`;
|
/seL4-l4v-10.1.1/HOL4/src/TeX/ |
H A D | mungeTools.sml | 360 (addz "\\\\", addz "\\begin{array}{c}", addz "\\end{array}")
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | type_grammar.sml | 40 array-typeshere) is mapped to abstract syntax, the ty_absyn type 516 [add_break(1,0), add_string " TY ::= TY[TY] (array type)"]
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootLib.sml | 141 (* Decide whether something is inside array bound *) 594 (* its an array*) 1465 (*destruct and search for points-to / array*) 1474 (*resort points-to/array to front*) 2134 (* array / interval - same start and length *) 2201 (* array / interval - split if necessary *) 2341 (* Converts points-to to an array *) 2964 (* 27.5 s *) val file = concat [examplesDir, "/interactive/array.dsf"];
|
/seL4-l4v-10.1.1/seL4/src/arch/x86/64/ |
H A D | traps.S | 667 # RSP points to the end of the VCPUs general purpose register array
|
/seL4-l4v-10.1.1/HOL4/examples/dev/AES/tupled/ |
H A D | sboxScript.sml | 126 This is just a one dimensional array indexed by words up to 256.
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Z3_ProofReplay.sml | 43 (* a simplification prover that deals with function (i.e., array) 850 val z3_th_lemma_array = th_lemma_wrapper "array" (fn (state, t) => 852 val thm = profile "th_lemma[array](3)(SIMP_PROVE_UPDATE)" 1039 list_prems state_proof "th_lemma[array]" z3_th_lemma_array x
|
/seL4-l4v-10.1.1/isabelle/src/HOL/SPARK/Manual/document/ |
H A D | intro.tex | 43 states that all elements of the array \texttt{a} with indices greater or equal to
|
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/SPARK/Manual/document/ |
H A D | intro.tex | 43 states that all elements of the array \texttt{a} with indices greater or equal to
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Foreign.sml | 307 (* Pass an ML vector as a pointer to a C array. *) 309 (* Pass an ML array as a pointer to a C array and, on return, update each element of 310 the ML array from the C array. *) 311 and cArrayPointer: 'a conversion -> 'a array conversion 1188 (* Word8Vector.vector to C array of bytes. It is only possible to 1189 do this one way because conversion from a C array requires 2414 (* Pass an ML vector as a pointer to a C array. *) 2445 (* Pass an ML array a [all...] |
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibArbnum.sml | 260 val q = Array.array(Int.+(m, 1), 0)
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | selftest.sml | 48 val _ = tprint "Parsing Datatype with bool-array type"
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | regexpMatch.sml | 304 let val _ = print "Mapping to array representation.\n"
|