/seL4-l4v-master/isabelle/src/Doc/Logics/document/ |
H A D | HOL.tex | 47 \it symbol & \it meta-type & \it priority & \it description \\ 106 equality. But equality has a high priority, as befitting a relation, while 107 if-and-only-if typically has the lowest priority. Thus, $\lnot\lnot P=P$ 225 \medskip All these binders have priority 10. 228 The low priority of binders means that they need to be enclosed in 250 Both \texttt{if} and \texttt{case} constructs have as low a priority as 465 \it symbol &\it name &\it meta-type & \it priority & \it description \\ 479 \it symbol & \it meta-type & \it priority & \it description \\ 1104 which associates to the right and has a lower priority than $*$: $\tau@1 + 1148 \it symbol & \it meta-type & \it priority [all...] |
H A D | LK.tex | 48 \it symbol &\it name &\it meta-type & \it priority & \it description \\ 66 \it symbol & \it meta-type & \it priority & \it description \\
|
H A D | CTT.tex | 108 \it symbol &\it name &\it meta-type & \it priority & \it description \\ 118 \it symbol & \it meta-type & \it priority & \it description \\ 656 \it symbol & \it meta-type & \it priority & \it description \\
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/ |
H A D | HOL.tex | 47 \it symbol & \it meta-type & \it priority & \it description \\ 106 equality. But equality has a high priority, as befitting a relation, while 107 if-and-only-if typically has the lowest priority. Thus, $\lnot\lnot P=P$ 225 \medskip All these binders have priority 10. 228 The low priority of binders means that they need to be enclosed in 250 Both \texttt{if} and \texttt{case} constructs have as low a priority as 465 \it symbol &\it name &\it meta-type & \it priority & \it description \\ 479 \it symbol & \it meta-type & \it priority & \it description \\ 1104 which associates to the right and has a lower priority than $*$: $\tau@1 + 1148 \it symbol & \it meta-type & \it priority [all...] |
H A D | LK.tex | 48 \it symbol &\it name &\it meta-type & \it priority & \it description \\ 66 \it symbol & \it meta-type & \it priority & \it description \\
|
H A D | CTT.tex | 108 \it symbol &\it name &\it meta-type & \it priority & \it description \\ 118 \it symbol & \it meta-type & \it priority & \it description \\ 656 \it symbol & \it meta-type & \it priority & \it description \\
|
/seL4-l4v-master/seL4/manual/parts/ |
H A D | objects.tex | 157 If there are no other runnable threads with the same priority as the caller, 284 allows scheduling context to be populated with parameters, which combined with priority
|
/seL4-l4v-master/HOL4/src/unwind/Manual/ |
H A D | description.tex | 367 The function also gives priority to non-internal lines when determining where
|
/seL4-l4v-master/isabelle/src/Doc/Logics_ZF/document/ |
H A D | FOL.tex | 65 \it symbol &\it name &\it meta-type & \it priority & \it description \\ 84 \it symbol & \it meta-type & \it priority & \it description \\
|
H A D | ZF.tex | 96 \it symbol & \it meta-type & \it priority & \it description \\ 1045 \it symbol & \it meta-type & \it priority & \it description \\ 1207 \it symbol & \it meta-type & \it priority & \it description \\ 1256 \it symbol & \it meta-type & \it priority & \it description \\ 1453 \it symbol & \it meta-type & \it priority & \it description \\ 1537 \it symbol & \it meta-type & \it priority & \it description \\
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics_ZF/document/ |
H A D | FOL.tex | 65 \it symbol &\it name &\it meta-type & \it priority & \it description \\ 84 \it symbol & \it meta-type & \it priority & \it description \\
|
H A D | ZF.tex | 96 \it symbol & \it meta-type & \it priority & \it description \\ 1045 \it symbol & \it meta-type & \it priority & \it description \\ 1207 \it symbol & \it meta-type & \it priority & \it description \\ 1256 \it symbol & \it meta-type & \it priority & \it description \\ 1453 \it symbol & \it meta-type & \it priority & \it description \\ 1537 \it symbol & \it meta-type & \it priority & \it description \\
|
/seL4-l4v-master/HOL4/src/quotient/src/ |
H A D | quotient.sml | 1535 | SOME (term_grammar.Infix (associativity, priority)) => 1538 Parse.add_infix(nam, priority, associativity) 1539 | SOME (term_grammar.Prefix priority) => 1543 fixity=Prefix priority, 1548 | SOME (term_grammar.Suffix priority) => 1552 fixity=Suffix priority,
|
/seL4-l4v-master/HOL4/examples/HolCheck/examples/ |
H A D | amba_ahbScript.sml | 282 (* arbiter: simple priority based *)
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | muSyntaxScript.sml | 60 (* overload ~,/\,\/,T and F give priority to the boolean versions *)
|
H A D | muCheck.sml | 1004 val (acts,acttbl) = ListPair.unzip (actns@dotactn) (* thus giving "." action last priority when pattern matching*)
|
/seL4-l4v-master/HOL4/examples/CCS/ |
H A D | CCSScript.sml | 339 val _ = overload_on ("+", ``sum``); (* priority: 500 *)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Thread.sml | 68 like scheduling priority. The current thread attributes control the
|
/seL4-l4v-master/HOL4/src/unwind/ |
H A D | unwindLib.sml | 465 (* gives them priority over the internal lines when the function is *)
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | fmapalScript.sml | 134 (* the basic list-combining function, which gives priority to the *)
|
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | foundations.tex | 989 $tac1$ priority:
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
H A D | foundations.tex | 989 $tac1$ priority:
|
/seL4-l4v-master/HOL4/src/probability/ |
H A D | iterateScript.sml | 1138 (* Fixes for tight_equality(): make sure the priority is slightly higher than
|
H A D | lebesgueScript.sml | 142 (* "<<" is already used in "src/n-bit/wordsScript.sml", same priority here *)
|