/seL4-l4v-10.1.1/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 121 proof typically relies on the general-purpose \textit{metis} proof method, which 268 \textit{smt} method call. Rough timings are shown in parentheses, indicating how 468 The \textit{metis}~(\textit{full\_types}) proof method 473 higher-order places (e.g., in set comprehensions). The method is automatically 516 a given prover and repeatedly calls a prover or proof method with subsets of 649 The \textit{metis} proof method has the syntax 1127 is the default encoding used by the \textit{metis} proof method. 1177 \textit{metis} proof method, the question mark is replaced by a 1186 \textit{metis} proof method, the `\hbox{??}' suffix is replaced by 1194 \textit{metis} proof method, th [all...] |
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Sledgehammer/document/ |
H A D | root.tex | 121 proof typically relies on the general-purpose \textit{metis} proof method, which 268 \textit{smt} method call. Rough timings are shown in parentheses, indicating how 468 The \textit{metis}~(\textit{full\_types}) proof method 473 higher-order places (e.g., in set comprehensions). The method is automatically 516 a given prover and repeatedly calls a prover or proof method with subsets of 649 The \textit{metis} proof method has the syntax 1127 is the default encoding used by the \textit{metis} proof method. 1177 \textit{metis} proof method, the question mark is replaced by a 1186 \textit{metis} proof method, the `\hbox{??}' suffix is replaced by 1194 \textit{metis} proof method, th [all...] |
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | fp.tex | 84 \commdx{apply}(\textit{method}), where \textit{method} is typically 88 assume that a method attacks merely the first subgoal. An exception is 202 A more general method for defining total recursive functions is introduced in 303 method that \isa{auto} always applies first, simplification.
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | fp.tex | 84 \commdx{apply}(\textit{method}), where \textit{method} is typically 88 assume that a method attacks merely the first subgoal. An exception is 202 A more general method for defining total recursive functions is introduced in 303 method that \isa{auto} always applies first, simplification.
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | threads.tex | 34 \apifunc{seL4\_Untyped\_Retype}{untyped_retype} method (see 42 or by seperately calling the \apifunc{seL4\_TCB\_Resume}{tcb_resume} method. In multicore machines, the thread 49 The \apifunc{seL4\_TCB\_Suspend}{tcb_suspend} method deactivates a thread. 85 \apifunc{seL4\_TCB\_Configure}{tcb_configure} method. 345 The \apifunc{seL4\_DomainSet\_Set}{domainset_set} method changes the domain
|
H A D | api.tex | 83 \newcommand{\noret}{This method does not return anything.}
|
H A D | cspace.tex | 44 these copied capabilities and the originals. The revoke method 107 capability in the second slot. The method is atomic; either both or 231 the mint method, a copy of the capability with a specific \emph{badge} can be 276 The \apifunc{seL4\_CNode\_Revoke}{cnode_revoke} method will
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics_ZF/document/ |
H A D | FOL.tex | 197 It instantiates the simplifier, which is invoked through the method 243 S$. The other \ldots\isa{\_impE} rules are unsafe; the method requires 265 \isa{tactic} method to call \ML{} tactics in an Isar script: 437 The theorem was proved in six method invocations, not counting the 467 \isa{unfold} method, which expands 596 \methdx{blast} method, which automatically uses the classical form
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics_ZF/document/ |
H A D | FOL.tex | 197 It instantiates the simplifier, which is invoked through the method 243 S$. The other \ldots\isa{\_impE} rules are unsafe; the method requires 265 \isa{tactic} method to call \ML{} tactics in an Isar script: 437 The theorem was proved in six method invocations, not counting the 467 \isa{unfold} method, which expands 596 \methdx{blast} method, which automatically uses the classical form
|
/seL4-l4v-10.1.1/HOL4/examples/imperative/ |
H A D | necec2010.sml | 301 \item{using an algebraic method in the case where s x and s y are numeric} 389 In the special case where both variables are numbers, an algebraic method can be used to swap the values without the use of a temporary variable.
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_editor.scala | 111 try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_editor.scala | 111 try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
|
/seL4-l4v-10.1.1/seL4/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/ |
H A D | syscalls.h | 23 #error Unknown method for kernel syscalls
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/ |
H A D | reductionScript.sml | 272 (* Define compatible relations on the term/method language. *) 629 (* We claim that RED1 is a binary relation on the object/method *) 752 (* We claim that RED is a binary relation on the object/method *) 902 (* We claim that REQUAL is a binary relation on the object/method *)
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Sup_Inf.sml | 3 (* DESCRIPTION : SUP-INF method for deciding a subset of Presburger *)
|
/seL4-l4v-10.1.1/isabelle/src/HOL/SPARK/Manual/document/ |
H A D | intro.tex | 55 \textbf{S}ummariser) that produces a table mentioning for each VC the method by which
|
/seL4-l4v-10.1.1/l4v/isabelle/src/HOL/SPARK/Manual/document/ |
H A D | intro.tex | 55 \textbf{S}ummariser) that produces a table mentioning for each VC the method by which
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 6 Resembling the method of semantic tableaux, the calculus is well suited for 661 These tactics use a method developed by Philippe de Groote. A subgoal is 664 The method is inherently depth-first.
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
H A D | LK.tex | 6 Resembling the method of semantic tableaux, the calculus is well suited for 661 These tactics use a method developed by Philippe de Groote. A subgoal is 664 The method is inherently depth-first.
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | tactics.tex | 63 Milner's particular contribution was in formalizing the method for 434 The second method is to compose 472 In general, the second method is both easier and more reliable. It is 1423 method provides no ready way of intercepting their arrival. 1438 method may result in bulky \ML{} expressions; and it may take some effort to present the text 1961 \noindent This gives the same result as the stack method, but more 2000 On the goal with the disjunctive antecedent, this method again 2020 a shorter expression than the direct method, which is: 2111 The new method has other applications as well, including as an 2122 \noindent Similarly, the method i [all...] |
/seL4-l4v-10.1.1/HOL4/src/quotient/Manual/ |
H A D | quotient.tex | 2280 %is known without giving a method for constructing it or identifying 4985 %and replacing an existing method in an object by another. 4995 We define the sets of object terms $O_1$ and method terms $M_1$ inductively as 5011 {\it method dictionary,} 5013 consisting of a label and a method. 5017 The form $a.l$ denotes the invocation of the method labelled $l$ in the 5019 $a$, where the method labelled $l$ (if any) is replaced by the new 5020 method $m$. The form $\varsigma(x)a$ denotes a method with one formal 5026 the object itself which contains this method [all...] |
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/binomial/ |
H A D | binomial.tex | 440 method is fine for small proofs, but in larger proofs it presents the problem 442 method is to put the predicates on the assumption list, and use resolution 773 an alternative method is to generate the subrange given its two endpoints,
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | tool.tex | 12 is very slow because of the `brute force' method used. The second 276 To implement this, a method of repeatedly applying a conversion to 1313 Use the `brute force' rewriting method described at the beginning of this chapter.
|
/seL4-l4v-10.1.1/HOL4/Manual/Tutorial/binomial/ |
H A D | binomial.tex | 440 method is fine for small proofs, but in larger proofs it presents the problem 442 method is to put the predicates on the assumption list, and use resolution 773 an alternative method is to generate the subrange given its two endpoints,
|
/seL4-l4v-10.1.1/HOL4/Manual/Tutorial/ |
H A D | tool.tex | 12 is very slow because of the `brute force' method used. The second 276 To implement this, a method of repeatedly applying a conversion to 1313 Use the `brute force' rewriting method described at the beginning of this chapter.
|