/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Graphview/ |
H A D | mutator_dialog.scala | 307 case Mutator.Edge_Endpoints((source, dest)) => 309 ("Source", new Text_Field_Input(source.ident)),
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Tptp.sig | 130 source : formulaSource}
|
/seL4-l4v-10.1.1/seL4/src/plat/pc99/machine/ |
H A D | acpi.c | 149 uint8_t source; member in struct:acpi_madt_iso 372 printf("ACPI: MADT_ISO bus=%d source=%d gsi=%d flags=0x%x\n", 374 ((acpi_madt_iso_t*)acpi_madt_header)->source,
|
/seL4-l4v-10.1.1/HOL4/Manual/Guide/ |
H A D | guide.tex | 105 source files for the \REFERENCE\ volume reside in the directory {\tt help}. The 134 \item {\tt Guide}: the \LaTeX\ source for the present document. 248 the \LaTeX\ source file {\tt index.tex} using the program {\tt makeindex}. 365 used to generate the \latex\ source for the manual entry on the identifier \id. 378 The source files for the manual are in the following subdirectories of the 423 that are used to generate the \LaTeX\ source for \REFERENCE\ from the \doc\ 426 \section{Generation of the LaTeX source} 429 \latex\ source for a manual entry on the \ML\ identifier \id\ can be generated. 431 source text from \doc\ files. Executing: 438 \latex\ source tex [all...] |
/seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
H A D | Logging.sml | 501 val (h,source) = dest_thm sth 502 val fvs = FVL (source::h) empty_varset 516 fun rconv fvs source template = (* |- source = template[rhs/vars] *) 517 ALPHA source template 522 val (sf,sa) = dest_comb source 527 val (sv,sb) = dest_abs source 534 val _ = log_thm (EQ_MP (rconv fvs source tm) sth)
|
/seL4-l4v-10.1.1/isabelle/src/Tools/VSCode/src/ |
H A D | state_panel.scala | 72 List(controls, HTML.source(text)), 137 tooltip = "Locate printed command within source text",
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | state_panel.scala | 72 List(controls, HTML.source(text)), 137 tooltip = "Locate printed command within source text",
|
/seL4-l4v-10.1.1/HOL4/tools-poly/ |
H A D | configure.sml | 111 replacement function: it searchs the source file for a line that 115 is done, the rest of the source is copied to the target. 279 doing anything in the source directory, tools/Holmake *) 502 output(tar4," au BufRead,BufNewFile *?Script.sml let maplocalleader = \"h\" | source "^tar1^"\n"); 504 output(tar4," \"au BufRead,BufNewFile *?Script.sml source "^fullPath [pref, "holabs.vim"]^"\n");
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | BoolArray.sml | 142 (* TODO: This only handles the case where the source starts at the beginning 143 of the vector. It is easy to modify it for the case where the source 169 (* This assumes that any extra bits of the source are 294 (* Copy all the source vectors into the destination. *) 413 source and destination are aligned on the same bit offset.
|
H A D | Word8Array.sml | 379 on the index whether the source and destination are the same or not. 397 val (source, i, l) = Word8VectorSlice.base src value 403 else System_move_str(source, d, offset + wordSize, diW, len)
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | ipc.tex | 196 \item A source capability cannot be looked up. Although the presence 197 of the source capabilities is checked when the sending thread 201 CSpace may have changed and the source capability pointers may
|
H A D | notifications.tex | 75 message source can be determined.
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | basic.sml | 227 (* Sanity check of the source program. *)
|
H A D | SALGen.sml | 312 ( print("STOP: The source program (FIL) includes structures whose conversion hasn't been implemented!\n"); 316 ( print("STOP: The source program (FIL) is invalid! (e.g. all variables are not of the same type)\n");
|
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | Theory.sig | 122 (* Theory files (which are just SML source code) call this function as
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | unix-systeml.sml | 5 can not depend on any other HOL source code. *)
|
H A D | winNT-systeml.sml | 5 absolutely can not depend on any other HOL source code. *)
|
/seL4-l4v-10.1.1/HOL4/tools-poly/Holmake/ |
H A D | unix-systeml.sml | 5 can not depend on any other HOL source code. *)
|
/seL4-l4v-10.1.1/HOL4/developers/ |
H A D | genUseScript.sml | 131 help = "Generate a poly-usable source file",
|
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | protocol.scala | 420 val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) 426 toks.map(tok => Symbol.encode(tok.source))): _*)
|
H A D | resources.scala | 34 /* source files of Isabelle/ML bootstrap */ 63 with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString)) 154 if (node_name.is_theory && reader.source.length > 0) {
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_rendering.scala | 107 else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2 108 else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | protocol.scala | 420 val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) 426 toks.map(tok => Symbol.encode(tok.source))): _*)
|
H A D | resources.scala | 34 /* source files of Isabelle/ML bootstrap */ 63 with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString)) 154 if (node_name.is_theory && reader.source.length > 0) {
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_rendering.scala | 107 else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2 108 else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
|