/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/ |
H A D | Makefile.in | 284 CLEANFILES = *.exe core* *.log *.sum
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Parse.sml | 34 val (bvs,core) = strip_forall Body 35 in (Bvar::bvs, core)
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/src/ |
H A D | riscv.spec | 641 -- Each register state is local to a core. 648 c_instret :: id -> regType -- per-core counters 670 -- ID of the core executing current instruction 678 -- core whose id equals procID. For example, writing "gpr(r)" refers 679 -- general purpose register "r" in the core whose id equals procID. 764 unit sendIPI(core::regType) = 765 { id = [core]::id 5035 -- This initializes each core (via setting procID appropriately) on
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Match.sml | 396 (* Support for the core regexp compiler. *)
|
H A D | Regexp_Type.sml | 1236 val core = value 1243 catlist (map byte2charset A @ core @ map byte2charset Z)
|
H A D | regexp_compilerScript.sml | 92 (* The core regexp compiler. The seen argument holds the already-seen *)
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibMeson.sml | 402 (* The core of meson: ancestor unification or Prolog-style extension. *)
|
/seL4-l4v-10.1.1/HOL4/examples/miller/subtypes/ |
H A D | subtypeTools.sml | 663 (* The core rewriting engine *)
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_coreScript.sml | 30 val milawa_core_tm = stringSyntax.fromMLstring (text_from_file "core.lisp");
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | CoarsestCongrScript.sml | 368 (* The shared core lemma used in PROP3's proof *)
|
/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | misc.tex | 84 There are three core functions, all in the \ml{Feedback} structure: 600 This option gives the user a way of over-riding code in the core distribution as the compiler will find their code before the distribution's. 788 This program takes a list of object files to include in a heap, an optional heap to build upon (use the \texttt{-b} command-line switch; the default is to use the heap behind the core \texttt{hol} executable), and an optional name for the new heap (the default is the traditional Unix \texttt{a.out}). 813 If the heap's dependencies are not core \HOL{} theories as they are here, then both the dependency line and the arguments to \texttt{buildheap} will need to be adjusted to link to the directory containing the files. 814 For core \HOL{} theories, the dependency has to mention the \texttt{SIGOBJ} directory, but when passing arguments to \texttt{buildheap}, that information doesn't need to be provided as \texttt{SIGOBJ} is always consulted by all \HOL{} builds.
|
H A D | QuantHeuristics.tex | 32 core, there is a modular, syntax driven search for instantiation.
|
H A D | holCheck.tex | 528 \(\mu\)-calculus model checking, in addition to having a model, also requires an environment: a mapping from variables to sets of states. The \hc{} core accepts environments as maps from strings to \texttt{term\_bdd}'s. However, the user interface for the moment has no provision for supplying an environment. This will be added in due course. In the meantime, environments can be ``faked'' by purely propositional subformulas, though this may not be particularly efficient.
|
H A D | HolBdd.tex | 99 rules as core infrastructure for building `fully-expansive' or
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | misc.tex | 84 There are three core functions, all in the \ml{Feedback} structure: 547 This option gives the user a way of over-riding code in the core distribution as the compiler will find their code before the distribution's. 723 This program takes a list of object files to include in a heap, an optional heap to build upon (use the \texttt{-b} command-line switch; the default is to use the heap behind the core \texttt{hol} executable), and an optional name for the new heap (the default is the traditional Unix \texttt{a.out}). 748 If the heap's dependencies are not core \HOL{} theories as they are here, then both the dependency line and the arguments to \texttt{buildheap} will need to be adjusted to link to the directory containing the files. 749 For core \HOL{} theories, the dependency has to mention the \texttt{SIGOBJ} directory, but when passing arguments to \texttt{buildheap}, that information doesn't need to be provided as \texttt{SIGOBJ} is always consulted by all \HOL{} builds.
|
H A D | QuantHeuristics.tex | 32 core, there is a modular, syntax driven search for instantiation.
|
H A D | holCheck.tex | 528 \(\mu\)-calculus model checking, in addition to having a model, also requires an environment: a mapping from variables to sets of states. The \hc{} core accepts environments as maps from strings to \texttt{term\_bdd}'s. However, the user interface for the moment has no provision for supplying an environment. This will be added in due course. In the meantime, environments can be ``faked'' by purely propositional subformulas, though this may not be particularly efficient.
|
H A D | HolBdd.tex | 99 rules as core infrastructure for building `fully-expansive' or
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | DEBUGGER_.sml | 228 the core language and STRUCTURES for the module language. *)
|
H A D | TYPEIDCODE.sml | 41 whereas type values are passed in the core language as an extra
|
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
H A D | ho_proverTools.sml | 1151 (* The core engine. *)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | coreScript.sml | 16 val _ = new_theory "core";
|
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/doc/ |
H A D | ds.tex | 258 Spatial formulae are the core of separation logic. They contain the
|
/seL4-l4v-10.1.1/HOL4/src/bool/ |
H A D | boolScript.sml | 309 val (bvs,core) = strip_forall Body 310 in ((Bvar::bvs), core)
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | logic.tex | 134 E' disponibile un'ampia collezione di costruttori e distruttori di termini per le teorie core di \HOL.
|