Searched refs:extension (Results 51 - 75 of 79) sorted by relevance

1234

/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/src/
H A Driscv.spec361 , 15-14 : MXS -- extension context status
462 , 15-14 : SXS -- extension context status
565 -- update extension context status
1020 -- machine host-target interface (berkeley extension)
1114 -- machine host-target interface (berkeley extension)
1226 -- machine host-target interface (berkeley extension)
5328 -- initialize extension context state
/seL4-l4v-master/HOL4/src/finite_maps/
H A DenumTacs.sml260 (ERR "DISPLAY_TO_set_CONV" "not a finite set extension") t;
H A DfmapalTacs.sml113 in extension than is provided by fmap; hence we supply here only
/seL4-l4v-master/HOL4/examples/algebra/polynomial/
H A DpolyCyclicScript.sml322 cyclotomic extension of Q.
/seL4-l4v-master/HOL4/src/probability/
H A DprobabilityScript.sml2390 (* 2. extension of `indep`: a sequence of pairwise independent events
2408 (* 3. extension of `indep`: a sequence of total independent events *)
2420 (* 5. extension of `indep_families`: pairwise independent sets/collections of events *)
2433 (* 6. extension of `indep_families`: total independent sets/collections of events *)
2448 (* 8. extension of `indep_rv`: pairwise independent random variables *)
2462 (* 9. extension of `indep-rv`: total independent random variables. *)
H A DmeasureScript.sml16 (* Caratheodory's extension theorem (real_measureTheory.CARATHEODORY) was *)
2242 (* Existence of Measure - Caratheodory's celebrated extension theorem *)
/seL4-l4v-master/HOL4/src/pred_set/Manual/
H A Ddescription.tex54 extension\/}\index{axiom of extension} for sets. This is not, of course,
/seL4-l4v-master/HOL4/examples/AKS/theories/
H A DAKSintroScript.sml967 Theorem: Given any poly p, there is "an extension field where p splits",
1225 "Let F be a field extension of F_p by a primitive r-th root of unity X"
H A DAKScleanScript.sml2241 Let F be a field extension of F_p by a primitive r-th root of unity X,
/seL4-l4v-master/HOL4/examples/algebra/finitefield/
H A DffPolyScript.sml1569 Of course, Field r is the extension field of (PF r), so this is extension of the same type.
H A DffAdvancedScript.sml1912 (* Define extension of a field to a different type *)
H A DffSplitScript.sml1581 (* Define polynomial extension *)
1768 (* Define the coprime extension based on ordz n (CARD R) *)
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/
H A Dproof-tools.tex682 \label{sec:dpll-applicability-extension}
/seL4-l4v-master/HOL4/Manual/Description/
H A Dversion2.tex631 \noindent is now provided by the parser/pretty-printer extension mentioned above.
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dversion2.tex631 \noindent is now provided by the parser/pretty-printer extension mentioned above.
/seL4-l4v-master/isabelle/src/Doc/Intro/document/
H A Dadvanced.tex702 demonstrating many of the theory extension features.
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/
H A Dadvanced.tex702 demonstrating many of the theory extension features.
/seL4-l4v-master/HOL4/src/relation/
H A DrelationScript.sml1055 * specialize it later to an extension of B.
/seL4-l4v-master/isabelle/src/Doc/Logics_ZF/document/
H A DZF.tex5 theory~\cite{halmos60,suppes72} as an extension of~\texttt{FOL}, classical
353 \tdx{extension}: A = B <-> A \isasymsubseteq B & B \isasymsubseteq A
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics_ZF/document/
H A DZF.tex5 theory~\cite{halmos60,suppes72} as an extension of~\texttt{FOL}, classical
353 \tdx{extension}: A = B <-> A \isasymsubseteq B & B \isasymsubseteq A
/seL4-l4v-master/HOL4/examples/temporal_deep/src/translations/
H A Dltl_to_automaton_formulaScript.sml904 (*The extension does not conflict with old
908 an extension.*)
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_logicScript.sml1238 (* PART 5: Soundness of context extension -- adding a new definition *)
/seL4-l4v-master/HOL4/examples/AKS/compute/
H A DcomputePolyScript.sml376 (* Simple MOD (unity k) -- just gives a weak extension
/seL4-l4v-master/HOL4/polyml/basis/
H A DFinalPolyML.sml913 (* Look to see if the file exists, possibly with an extension,
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/X86Code/
H A DX86FOREIGNCALL.sml1534 At least at the moment we ignore any sign extension. *)

Completed in 384 milliseconds

1234