Searched refs:single (Results 1 - 25 of 251) sorted by relevance

1234567891011

/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/
H A Dmsvcc.sh131 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 Dintro.tex20 \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 Darm_progLib.sml957 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 DtripleSyntax.sml34 | _ => raise ERR "get_component" "not single hyp"
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DThyDataSexp.sig25 new data (representing a single key-value maplet) should be a singleton
/seL4-l4v-10.1.1/HOL4/tools/
H A Dunquote-init.sml8 even for files that contain single quotes because of the special
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DProof.sig24 (* Reconstructing single inferences. *)
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DProof.sig24 (* Reconstructing single inferences. *)
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DUnwind.sig9 * 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 DboolSimps.sig45 much as possible of STRIP_TAC within a single goal.
/seL4-l4v-10.1.1/HOL4/src/floating-point/native/
H A Dselftest.sml215 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 Dcomputer.ml9 % 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 DGetOpt.sig15 * 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 DGetOpt.sig18 * 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 Dthreads.tex262 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 DMenuBase.sml66 (* Sometimes we just want a single flag - either MF_BYCOMMAND or MF_BYPOSITION
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A Dlocn.sig36 (* single-point region *)
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/
H A DBuildAll.sml36 to be pasted into a window as a single item. Otherwise the
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/scripts/
H A Dmlpp293 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 DSingleAssignment.sml2 Title: References that allow a single assignment
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/scripts/
H A Dmlpp293 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 Dfinite_test_setScript.sml8 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 DTEA.sml7 (* 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 Ddataabs.ml5 % logic to boolean logic for single bits and for %
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/
H A DSequents.tex110 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'},

Completed in 109 milliseconds

1234567891011