/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | msvcc.sh | 131 single="-c" 184 if [ -n "$single" ]; then 238 args="-nologo $safeseh $single $output $ppsrc"
|
/seL4-l4v-10.1.1/l4v/camkes/adl-spec/document/ |
H A D | intro.tex | 20 \item \emph{Multiple instantiation of a single component.} Multiple copies of 23 \item \emph{Multiple implementations of an interface.} A single component can
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/prog/ |
H A D | arm_progLib.sml | 957 arm_spec "VLDR (single,+imm,pc)" 959 arm_spec "VLDR (single,-imm,pc)" 970 arm_spec "VMOV (single,reg)"; 972 arm_spec "VMOV (single,imm)"; 974 arm_spec "VMOV (single from arm)"; 975 arm_spec "VMOV (single to arm)"; 981 arm_spec "VCMP (single,zero)"; 983 arm_spec "VCMP (single)"; 986 arm_spec "VCVT (single,double)"; 987 arm_spec "VCVT (double,single,l [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | tripleSyntax.sml | 34 | _ => raise ERR "get_component" "not single hyp"
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | ThyDataSexp.sig | 25 new data (representing a single key-value maplet) should be a singleton
|
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | unquote-init.sml | 8 even for files that contain single quotes because of the special
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sig | 24 (* Reconstructing single inferences. *)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Proof.sig | 24 (* Reconstructing single inferences. *)
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Unwind.sig | 9 * is restricted to a single point via an equality in the 25 * is restricted to a single point via an equality in the
|
H A D | boolSimps.sig | 45 much as possible of STRIP_TAC within a single goal.
|
/seL4-l4v-10.1.1/HOL4/src/floating-point/native/ |
H A D | selftest.sml | 215 val () = test_monops ``:single`` 216 val () = test_binops ``:single`` 217 val () = test_orderings ``:single``
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/ |
H A D | computer.ml | 9 % computer which results from the execution of a single target level % 27 % a single point in time. %
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | GetOpt.sig | 15 * and the recognition of long options with a single dash (e.g. '-help' is 61 (* Description of a single option *)
|
/seL4-l4v-10.1.1/l4v/tools/c-parser/standalone-parser/ |
H A D | GetOpt.sig | 18 * and the recognition of long options with a single dash (e.g. '-help' is 64 (* Description of a single option *)
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | threads.tex | 262 single-step faults.} 268 The kernel provides support for the use of hardware single-stepping of userspace 273 an instruction breakpoint, to use when setting up the single-stepping 276 register to provide single-stepping functionality. If the caller's hardware platform requires the 279 breakpoint to provide single-stepping, seL4 will return \texttt{false} in \texttt{bp\_was\_consumed} and 284 the caller has disabled single-stepping and released that register, via a subsequent 287 \textbf{disables single stepping}. 290 single-stepping functionality, seL4 will restrict the number of registers that 291 can be configured as single-steppers, to one at any given time. The register that 292 is currently configured (if any) for single [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | MenuBase.sml | 66 (* Sometimes we just want a single flag - either MF_BYCOMMAND or MF_BYPOSITION
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | locn.sig | 36 (* single-point region *)
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/ |
H A D | BuildAll.sml | 36 to be pasted into a window as a single item. Otherwise the
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 293 Concatenates the input list of SML source files into a single file 295 concatenating into a single file.
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | SingleAssignment.sml | 2 Title: References that allow a single assignment
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/scripts/ |
H A D | mlpp | 293 Concatenates the input list of SML source files into a single file 295 concatenating into a single file.
|
/seL4-l4v-10.1.1/HOL4/examples/finite-test-set/ |
H A D | finite_test_setScript.sml | 8 UOK "solved" by a single instance. 20 UOK Thus, every first-order formula can be decided by checking a single instance. 25 UOK Rather than a single instance, they show solvability by a finite test set. 44 variables and a single Sheffer connective. 111 (* Solvability by a single instance *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/examples/ |
H A D | TEA.sml | 7 (* rounds before a single bit change of the data or key has spread very *)
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/mos-count/ |
H A D | dataabs.ml | 5 % logic to boolean logic for single bits and for %
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | Sequents.tex | 110 form of sequents required: single or multiple conclusions. So 165 external representations are the ones used for, say single and 179 \item The \ML{} functions \texttt{single\_tr}, \texttt{two\_seq\_tr}, 182 \texttt{single\_tr'}, \texttt{two\_seq\_tr'}, \texttt{three\_seq\_tr'},
|