| /seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
| H A D | isabelle_sidekick.scala | 196 val content = command.source(info.range).replace('\n', ' ')
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
| H A D | isabelle_sidekick.scala | 196 val content = command.source(info.range).replace('\n', ' ')
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | polytypicLib.sml | 994 (* 'source' function deals with encoding *)
1173 "\nis not a valid source or target function",
1180 "\nis not a fully expanded source or target function,\n" ^
1925 (* Tests for the existence of a source function, adds a new source *)
1932 (* Tests for the existence of a source theorem, adds a new source *)
1933 (* theorem and returns a source theorem. *)
2144 (*-- source functions and theorems --*)
2157 ("No source function
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/unwind/ |
| H A D | unwindLib.sml | 543 fun next_comb_at_this_level source n (h::t) =
544 let val l = list_after h source
547 else next_comb_at_this_level source (n + 1) t
551 fun next_combination source previous =
552 next_comb_at_this_level source 0 previous
553 handle HOL_ERR _ => rev_front_of source ((length previous) + 1) []
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | problem.py | 439 def is_reachable_from (self, source, target):
441 from starting node "source"'''
442 k = ('is_reachable_from', source)
449 visit = [source]
|
| /seL4-l4v-10.1.1/seL4/src/arch/x86/object/ |
| H A D | vcpu.c | 1218 vcpu_gp_register_t source = crExitRegs[vmx_data_exit_qualification_control_regster_get_reg(qual)]; local
1220 if (source == VCPU_ESP) {
1226 value = NODE_STATE(ksCurThread)->tcbArch.tcbVCPU->gp_registers[source];
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/ |
| H A D | darwin.S | 211 addi r4,r28,LINKAGE_SIZE ; source
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | BackendIntermediateCode.sml | 574 val source = BoolVector.length filter value
579 PrettyString (concat["SETCONTAINER(", Int.toString dest, "/", Int.toString source, ", "]),
|
| H A D | BaseCodeTree.sml | 454 val source = BoolVector.length filter value
459 string (concat["SETCONTAINER(", Int.toString dest, "/", Int.toString source, ", "]),
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/Tools/ |
| H A D | imports.scala | 80 val s1 = tok.source
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
| H A D | imports.scala | 80 val s1 = tok.source
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
| H A D | compiler.sml | 147 (* Compiling a list of source functions. *)
|
| H A D | regAlloc.sml | 653 (* alpha-equivalent to the source program. *)
694 ( print("The source program is invalid!\
|
| /seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/ |
| H A D | for_compileScript.sml | 441 (* We prove that phase 2 preserves semantics if the source semantics
845 (* We prove that phase3 preserves semantics if the source does not
902 that is identical to the source program, if the course program does
918 source program cannot Crash. This leads to a cleaner top-level
|
| H A D | for_nd_compileScript.sml | 462 the source semantics does not contain Crash (implied by successful
962 (* We prove that phase3 preserves semantics if the source does not
1048 behaviour of the source code, if Crash is not an observable
1069 that the source program cannot Crash. This leads to a cleaner
|
| /seL4-l4v-10.1.1/HOL4/polyml/samplecode/ide/ |
| H A D | use.sml | 45 For each source file within this directory with path a/b/c.ML there will be a
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Ho_Rewrite.sml | 194 * Taken directly from the GTT source code (Don Syme).
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | Holdep.sml | 2 source files. Also has knowledge of HOL script and theory files.
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/examples/ |
| H A D | example_axiomsScript.ml | 276 First, the comment inside the axiom itself (in source file axioms.lisp)
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/VSCode/src/ |
| H A D | protocol.scala | 470 severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None)
476 JSON.optional("source" -> source)
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/VSCode/src/ |
| H A D | protocol.scala | 470 severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None)
476 JSON.optional("source" -> source)
|
| /seL4-l4v-10.1.1/seL4/manual/parts/ |
| H A D | api.tex | 195 \ipcbloc{IPCBuffer[0]} & 1 if the lookup failed for a source capability, 0 otherwise\\
|
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | misc.tex | 45 \HOL{} source, one can get a listing of the entrypoints found in the
65 \verb+help "Tactic"+ & \HOL{} source structure information \\
107 source directory. A single invocation of \holmake{} will compute
649 system's overlay file. This is needed for compilation of HOL source
779 In Moscow~ML, \texttt{hol} starts up by visibly (and relatively slowly) ``loading'' the various source files that provide the system's functionality (\eg, \ml{bossLib}).
782 Such heaps can be preloaded with source code implementing special-purpose reasoning facilities, and with various necessary background theories.
796 For example, the \texttt{realheap} above might be generated with the source in Figure~\ref{fig:realheap-makefile}.
962 The commands are not really processed by \LaTeX{}: instead the source file must first be passed through the \munge{} filter.
984 \paragraph{Before starting} In order to use the munger, one must ``include'' (use the \texttt{\bs{}usepackage} command) the \texttt{holtexbasic.sty} style-file, which is found in the HOL source directory \texttt{src/TeX}.
1489 of the \LaTeX{} source fil
[all...] |
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | misc.tex | 45 \HOL{} source, one can get a listing of the entrypoints found in the
65 \verb+help "Tactic"+ & \HOL{} source structure information \\
107 source directory. A single invocation of \holmake{} will compute
587 system's overlay file. This is needed for compilation of HOL source
714 In Moscow~ML, \texttt{hol} starts up by visibly (and relatively slowly) ``loading'' the various source files that provide the system's functionality (\eg, \ml{bossLib}).
717 Such heaps can be preloaded with source code implementing special-purpose reasoning facilities, and with various necessary background theories.
731 For example, the \texttt{realheap} above might be generated with the source in Figure~\ref{fig:realheap-makefile}.
893 The commands are not really processed by \LaTeX{}: instead the source file must first be passed through the \munge{} filter.
915 \paragraph{Before Starting} In order to use the munger, one must ``include'' (use the \texttt{\bs{}usepackage} command) the \texttt{holtexbasic.sty} style-file, which is found in the HOL source directory \texttt{src/TeX}.
1306 of the \LaTeX{} source fil
[all...] |
| /seL4-l4v-10.1.1/HOL4/tools/ |
| H A D | configure.sml | 92 replacement function: it searchs the source file for a line that
96 is done, the rest of the source is copied to the target.
|