| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
| H A D | Message.sml | 1392 | WM_QUERYENDSESSION of { source: int }
1890 | decompileMessage ( 0x0011, wp, _) = WM_QUERYENDSESSION { source = SysWord.toInt wp }
2663 | compileMessage (WM_QUERYENDSESSION { source}) = (0x0011, SysWord.fromInt source, 0w0, noFree)
|
| /seL4-l4v-10.1.1/HOL4/tools/ |
| H A D | buildutils.sml | 600 the strings are source and destination file-names, in that order
|
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | QuantHeuristics.tex | 538 at the source code and contact Thomas Tuerk
|
| H A D | holCheck.tex | 212 The numeric argument to \(\mathtt{ttt.makeTTT}\) gives the size of grid required. Now we consider each component of the model \texttt{ttt1}, using the \texttt{holCheckLib.get\_*} family of functions. The corresponding \texttt{holCheckLib.set\_*} functions were used to actually construct the model. The argument to each \texttt{set} function is precisely the return value of the corresponding \texttt{get} function as seen below. The only difference is that the values of optional model components are returned as option types. See the source code of \texttt{mod8.sml} in the HolCheck \texttt{examples} directory for a simple example of how this is done. See \S\ref{sec:models} for general details on model construction.
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | QuantHeuristics.tex | 528 at the source code and contact Thomas Tuerk
|
| H A D | holCheck.tex | 212 The numeric argument to \(\mathtt{ttt.makeTTT}\) gives the size of grid required. Now we consider each component of the model \texttt{ttt1}, using the \texttt{holCheckLib.get\_*} family of functions. The corresponding \texttt{holCheckLib.set\_*} functions were used to actually construct the model. The argument to each \texttt{set} function is precisely the return value of the corresponding \texttt{get} function as seen below. The only difference is that the values of optional model components are returned as option types. See the source code of \texttt{mod8.sml} in the HolCheck \texttt{examples} directory for a simple example of how this is done. See \S\ref{sec:models} for general details on model construction.
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | muCheck.sml | 863 (*preimg of img cut to b2 is all source states *)
865 in bdd.AND(pi,b1) end (* cut down source states to the ones in b1 *)
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | CODETREE_SIMPLIFIER.sml | 399 val _ = reprocess := true (* Frequently the source will be a constant. *)
402 (* We don't know if the source is immutable but the destination definitely isn't *)
|
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | FinalPolyML.sml | 170 location than a source line. Default: fn () => 0 i.e. no line numbering. *)
913 (* If the object is a directory the source is in the bind file. *)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | preARMScript.sml | 153 (* An instruction: ((operator, condition code, set flags), destination, source, jump) *)
|
| H A D | ARMCompositionScript.sml | 415 (* of the source state *)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | preARMScript.sml | 149 (* An instruction: ((operator, condition code, set flags), destination, source, jump) *)
|
| H A D | ARMCompositionScript.sml | 415 (* of the source state *)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | preARMScript.sml | 147 (* An instruction: ((operator, condition code, set flags), destination, source, jump) *)
|
| H A D | ARMCompositionScript.sml | 429 (* of the source state *)
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/Manual/ |
| H A D | paper.tex | 869 on this work is in preparation, and the {\small HOL} source code for the
|
| /seL4-l4v-10.1.1/HOL4/tools/mllex/ |
| H A D | mllex.sml | 66 * both SML/NJ and MLton. The source code is also compilable by mlton,
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/binomial/ |
| H A D | binomial.tex | 96 in the form displayed by \HOL{}, rather than as \ML{} source text. Specific
|
| /seL4-l4v-10.1.1/HOL4/Manual/Tutorial/binomial/ |
| H A D | binomial.tex | 96 in the form displayed by \HOL{}, rather than as \ML{} source text. Specific
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
| H A D | texinfo.tex | 26 % a Texinfo source document, you may use the result without
4091 { \catcode`_=11 % We want to use \_STOP_ which cannot appear in texinfo source.
4393 % Sample source (mac-idx3.tex, reported by Graham Percival to
4917 % Index files are almost Texinfo source, but we use \ as the escape
6772 % beforehand -- and a) we want @copying to be done first in the source
9794 % your texinfo source file like this:
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/ |
| H A D | ind_types.sml | 8 (* ported from Caml Light source by Michael Norrish, November 1999 *)
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | xwindows.cpp | 1915 Pixmap source,
1923 return EmptyCursor(taskData, dsHandle,XCreatePixmapCursor(DEREFDISPLAYHANDLE(dsHandle)->display,source,mask,foreground,background,x,y));
7529 GetPixmap(taskData, XP1), /* source */
1911 CreatePixmapCursor( TaskData *taskData, Handle dsHandle, Pixmap source, Pixmap mask, XColor *foreground, XColor *background, unsigned x, unsigned y ) argument
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Sledgehammer/document/ |
| H A D | root.tex | 119 The result of a successful proof search is some source text that usually (but
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Sledgehammer/document/ |
| H A D | root.tex | 119 The result of a successful proof search is some source text that usually (but
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
| H A D | x64.sml | 6032 else FAIL "expecting 32-bit or 64-bit register source")
6176 FAIL "SETcc requires byte source"
|