/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | theories.tex | 1342 \index{ zero, nella logica HOL@\ml{0} (zero, nella logica \HOL{})} 1845 ottali sono quelli che appaiono con gli zero in testa. 1882 `\ml{SUC}' per qualsiasi numerale diverso da zero. Per esempio: 2003 componente non deve essere zero. Per rendere le cose pi� semplici nella teoria \HOL\, 2222 che � impossibile introdurre word di lunghezza zero perch� tutti i tipi 2252 persi (esegue un'estrazione di bit), altrimenti la parola pi� lunga avr� lo stesso valore dell'originale (fornendo in effetti zero padding). 2331 L'ordinamento di un bit di parola pu� essere capovolto con \holtxt{word\_reverse}, cio� il bit zero � scambiato con il bit $n - 1$ e cos� via. 2461 \holtxt{word\_slice} & \holtxt{''} & \num\rarr\num\rarr\worda\rarr\worda & Set bits outside field to zero \\ 3484 La traccia utente (si veda la Sezione~\ref{sec:traces}) \ml{"Univ~pretty-printing"} pu� essere impostata a zero pe [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/ |
H A D | texinfo.tex | 1338 \def\numsubsubsecentry##1##2##3##4{% count is always zero 2213 % Computer Modern typewriter fonts have zero interword stretch (and 3664 % done a \vskip-\parskip. In that case, we don't want to zero 3667 % usually is), we do want to zero parskip, or there would be too much 4782 % \write or \pdfdest will make \lastskip zero. The result is that 4797 % We'll have to check whether \lastskip is zero skip. \ifdim is not 4833 % If \lastskip was zero, perhaps the last item was a penalty, and 5421 % all lower-level sectioning counters to zero. 5929 \hangindent=\wd0 % zero if no section number 6306 % is reset to zero; thu [all...] |
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | WeakEQScript.sml | 1798 (* `EPS E E1` implies zero or more tau transitions, and this leads to 1799 zero or at least one tau transition on the other side, which implies
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_OPTIMISER.sml | 1130 immediately we try to expand it unless maxInlineSize is zero. We 1312 reconstruct one with unused fields set to zero. They will
|
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | document.scala | 1084 val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | document.scala | 1084 val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Pmatch.sml | 767 | _ => msg("The following input rows (counting from zero) are\
|
H A D | Tactic.sml | 418 * where each y is a vector of zero or more variables and each Bi is a *
|
H A D | Conv.sml | 24 icdomain/zero/1.0/legalcode>. This should not be interpreted as a personal 290 * Apply a conversion zero or more times. *
|
H A D | selftest.sml | 871 val _ = new_constant ("zero", ``:num``)
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | int_arithScript.sml | 264 (* c zero *)
|
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/ |
H A D | reductionScript.sml | 709 (* in zero or more steps, as defined in Barendregt, Definition 3.1.5, *)
|
/seL4-l4v-10.1.1/HOL4/src/rational/ |
H A D | fracScript.sml | 162 * some useful things about positive and non-zero
|
/seL4-l4v-10.1.1/HOL4/examples/lambda/other-models/ |
H A D | ncScript.sml | 265 let val sth = Q.SPECL [`\k. (F,F)`, (* map CON to zero *)
|
/seL4-l4v-10.1.1/isabelle/src/Doc/Tutorial/document/ |
H A D | fp.tex | 180 \item zero for all constructors that do not have an argument of type $t$,
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | fp.tex | 180 \item zero for all constructors that do not have an argument of type $t$,
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | BasicStreamIO.sml | 73 vector has size zero this is treated as EOF.
|
H A D | FinalPolyML.sml | 174 the current file, a byte offset or simply zero. 232 zero means no profiling and one means add the allocating function. *)
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | seqScript.sml | 553 (* Prove a sequence tends to zero iff its abs does *) 945 (* Series which is zero beyond a certain point *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/decompiler/ |
H A D | decompilerLib.sml | 556 val zero = ([0],exit) value 558 then zs @ [zero]
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | preARMScript.sml | 30 (* Z - the result was zero *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
H A D | preARMScript.sml | 27 (* Z - the result was zero *)
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
H A D | preARMScript.sml | 26 (* Z - the result was zero *)
|
/seL4-l4v-10.1.1/HOL4/src/IndDef/Manual/ |
H A D | paper.tex | 395 are \mbox{exactly} those numbers obtainable from zero by adding multiples of
|
/seL4-l4v-10.1.1/HOL4/src/list/src/ |
H A D | ListConv1.sml | 685 val length = len Arbnum.zero list
|