| /seL4-l4v-master/l4v/isabelle/src/HOL/Data_Structures/document/ |
| H A D | root.tex | 58 The functional version is due to Hinze~\cite{Hinze-bro12}.
|
| /seL4-l4v-master/isabelle/src/HOL/Data_Structures/document/ |
| H A D | root.tex | 58 The functional version is due to Hinze~\cite{Hinze-bro12}.
|
| /seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
| H A D | DEBUG.sig | 6 License version 2.1 as published by the Free Software Foundation.
|
| /seL4-l4v-master/HOL4/developers/ |
| H A D | prehol.sml | 169 ^Globals.release^" "^Lib.int_to_string(Globals.version)^build_stamp
214 * A version of "use" that filters quotations. The native MoscowML version *
|
| /seL4-l4v-master/HOL4/examples/Crypto/Serpent/Reference/ |
| H A D | Serpent_Reference_KeyScheduleScript.sml | 52 A version with mainly bit shifts, rotation and bitwise operation has been tried,
92 (*this is the key used in the optimized version*)
97 (*this is the key used in the reference version*)
|
| /seL4-l4v-master/isabelle/src/Tools/VSCode/src/ |
| H A D | protocol.scala | 289 version <- JSON.long(doc, "version")
291 } yield (Url.absolute_file(uri), lang, version, text)
311 version <- JSON.long(doc, "version")
313 } yield (Url.absolute_file(uri), version, changes)
342 sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit])
346 "textDocument" -> JSON.Object("uri" -> Url.print_file(file), "version" -> version),
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/ |
| H A D | protocol.scala | 289 version <- JSON.long(doc, "version")
291 } yield (Url.absolute_file(uri), lang, version, text)
311 version <- JSON.long(doc, "version")
313 } yield (Url.absolute_file(uri), version, changes)
342 sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit])
346 "textDocument" -> JSON.Object("uri" -> Url.print_file(file), "version" -> version),
|
| /seL4-l4v-master/l4v/isabelle/src/Doc/Sledgehammer/document/ |
| H A D | root.tex | 126 Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on
196 \texttt{LEO3\_VERSION}, or \texttt{SATALLAX\_VERSION} to the prover's version
208 \texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0'').
461 We hope to address this problem in a future version of Isabelle. In the
739 with version 1.0.
757 prebuilt CVC4 package from \download. Sledgehammer has been tested with version
763 executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or
775 \item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of
783 executable. Sledgehammer has been tested with version 2.8. iProver depends on
790 \texttt{leo} executable. Sledgehammer requires version 1.
[all...] |
| /seL4-l4v-master/isabelle/src/Doc/Sledgehammer/document/ |
| H A D | root.tex | 126 Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on
196 \texttt{LEO3\_VERSION}, or \texttt{SATALLAX\_VERSION} to the prover's version
208 \texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0'').
461 We hope to address this problem in a future version of Isabelle. In the
739 with version 1.0.
757 prebuilt CVC4 package from \download. Sledgehammer has been tested with version
763 executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or
775 \item[\labelitemi] \textbf{\textit{ehoh}:} Ehoh is an experimental version of
783 executable. Sledgehammer has been tested with version 2.8. iProver depends on
790 \texttt{leo} executable. Sledgehammer requires version 1.
[all...] |
| /seL4-l4v-master/HOL4/src/coretypes/pair-Manual/ |
| H A D | description.tex | 41 The pair library contains a version of every standard \HOL\ function
214 Note that it is always possible to use the paired version
215 of an inference rule in place of the standard version.
238 short example that exhibits the bug and the version number of the
240 The constant \mbox{\tt pair\_version} contains the version number of the pair
|
| /seL4-l4v-master/HOL4/src/pattern_matches/ |
| H A D | patternMatchesLib.sig | 174 (* There is also a more generic version that
370 (* A simplified version of PMATCH_CASE_SPLIT_CONV that
385 it needs to get the current version of the default db,
504 the fast version with the power of the slow one.
573 (* A generalised version that allows specifying additional
588 also a version that returns an exhaustiveness statement of the
|
| /seL4-l4v-master/HOL4/polyml/basis/ |
| H A D | PrimIO.sml | 8 version 2.1 of the License, or (at your option) any later version.
229 (* No blocking version exists - try using block and the
230 synthesised non-blocking version. *)
414 (* No blocking version exists - try using block and the
415 synthesised non-blocking version. *)
|
| /seL4-l4v-master/HOL4/Manual/Description/ |
| H A D | HolQbf.tex | 33 \ml{HolQbfLib} has been tested with (the x86 Linux version of) Squolem
34 2.02 (release date 2010-11-10). This is Squolem's latest version at
141 (parts of) the QDIMACS standard, version 1.1 (released on December~21,
|
| /seL4-l4v-master/HOL4/Manual/Translations/IT/Description/ |
| H A D | HolQbf.tex | 33 \ml{HolQbfLib} has been tested with (the x86 Linux version of) Squolem
34 2.02 (release date 2010-11-10). This is Squolem's latest version at
138 (parts of) the QDIMACS standard, version 1.1 (released on December~21,
|
| /seL4-l4v-master/HOL4/examples/AKS/compute/ |
| H A D | computeAKSScript.sml | 415 (* Note: the following is a weak version.
416 The strong version is:
422 -- the strong version is: aks_compute_alt.
|
| /seL4-l4v-master/HOL4/examples/dev/AES/word8/ |
| H A D | MultScript.sml | 65 (* Iterative version *)
|
| /seL4-l4v-master/HOL4/examples/elliptic/ |
| H A D | Stream.sml | 3 (* Copyright (c) 2001-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
|
| /seL4-l4v-master/HOL4/examples/hardware/hol88/computer/ |
| H A D | computer.ml | 14 % part of the verification procedure. The final version of the %
|
| /seL4-l4v-master/HOL4/examples/hardware/hol88/ |
| H A D | mk_Luis.ml | 142 First we delete the version of LUIS_THM stored in the current theory. %
|
| /seL4-l4v-master/HOL4/examples/ind_def/ |
| H A D | monosetScript.sml | 60 now we define our own version EVERY, putting the arguments in a
|
| /seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
| H A D | Path.sml | 7 License version 2.1 as published by the Free Software Foundation.
|
| /seL4-l4v-master/HOL4/src/HolSmt/ |
| H A D | Z3_Proof.sml | 21 that the most recent Z3 version (2.11) uses. I have applied Z3
|
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibPatricia.sml | 7 (* License version 2, as published by the Free Software Foundation. *)
|
| /seL4-l4v-master/HOL4/src/num/arith/src/ |
| H A D | numSimps.sig | 82 [old_ARITH_ss] is an old version of ARITH_ss that does less
|
| /seL4-l4v-master/HOL4/tools/mlyacc/mlyacclib/ |
| H A D | MLY_parser1.sml | 26 but it is wastes space in the release version.
|