/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_logicScript.sml | 255 val zero = ``mConst (Val 0)`` value 348 (^pequal (^add [^a;^b]) (^add [^zero;^b]))); 349 (* Axiom 31. plus-of-zero-when-natural *) 351 (^pequal (^add [^a;^zero]) ^a)); 357 (* Axiom 34. less-of-zero-right *) 358 (^pequal (^less [^a;^zero]) ^nnil); 359 (* Axiom 35. less-of-zero-left-when-natp *) 361 (^pequal (^less [^zero;^a]) (^iff [^eequal [^a;^zero];^nnil;^t]))); 364 (^pequal (^less [^a;^b]) (^less [^zero; [all...] |
/seL4-l4v-10.1.1/HOL4/examples/computability/turingMachines/ |
H A D | register_machineScript.sml | 145 Clear (r) = set r to zero
|
/seL4-l4v-10.1.1/HOL4/examples/hardware/hol88/computer/ |
H A D | proof4.ml | 189 % Case: run, button = F, zero, opcode is 2 (JZR) ====================== %
|
H A D | proof6.ml | 37 % 'abs_zero' is a constant defining the zero case predicate in the % 47 % 'abs_non_zero' is a constant defining the non-zero case predicate %
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | Painting.sml | 119 (* If the update area is empty the result is zero. *)
|
H A D | Bitmap.sml | 294 argument and setting bitsPerPixel to zero in the BITMAPINFO argument 295 simply fills in the BITMAPINFOHEADER. With bitsPerPixel non-zero it
|
/seL4-l4v-10.1.1/HOL4/src/rational/ |
H A D | ratSyntax.sml | 186 val (n, f) = if Arbint.<(i,Arbint.zero) then (Arbint.~ i, mk_rat_ainv)
|
/seL4-l4v-10.1.1/HOL4/src/real/ |
H A D | realSyntax.sml | 80 if Arbint.<(i,Arbint.zero) then mk_negated(posint(Arbint.~ i))
|
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/ |
H A D | res_quanLib.sig | 17 main/zero/1.0/legalcode>. This should not be interpreted as a personal
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_compilerLib.sml | 17 val counter = ref (Arbnum.zero)
|
/seL4-l4v-10.1.1/HOL4/Manual/Quick/ |
H A D | quick.tex | 182 \hol{Drule}{SPECL} [\var{terms}] & specializes zero or more variables in the conclusion of a theorem \\ 186 \hol{Drule}{ISPECL} [\var{terms}] & specializes theorem zero or more times, with type instantiation if necessary \\ 189 \hol{Drule}{GENL} [\var{terms}] & generalizes zero or more variables in the conclusion of a theorem \\ 210 \hol{numLib}{num_CONV} & equates a non-zero numeral with the form $\mathrm{SUC}\ x$ for some $x$ \\
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | json.scala | 108 (zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^ 117 def zero = one(character(c => c == '0'))
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | BoolArray.sml | 77 (* Make a array initialised to zero. *) 170 zero. *) 184 (* TODO: If dest_bit is zero we can simply move the bytes. If len 417 (* Copy one array into another. The arrays could be the same but in that case di must be zero. *)
|
H A D | Thread.sml | 267 Word 4: Maximum ML stack size. Unlimited is stored here as zero 314 will be non-zero. *) 335 if n <= 0 then raise Thread "The stack size must be greater than zero" else n 443 by zero but if it was already locked it will be some negative value. When it 446 zero or negative. In that case the unlocking thread needs to call in to the
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | json.scala | 108 (zero | positive) ~ opt(number_fract) ~ opt(number_exp) ^^ 117 def zero = one(character(c => c == '0'))
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | Feedback.sml | 185 then raise ERR "register_trace" "Can't have trace values less than zero." 231 "Can't have trace values less than zero."
|
/seL4-l4v-10.1.1/HOL4/src/res_quan/Manual/ |
H A D | summary.tex | 187 Generalizes zero or more variables to restricted universal quantification 209 Specializes zero or more variables in the conclusion of a restricted
|
/seL4-l4v-10.1.1/HOL4/src/n-bit/ |
H A D | blastLib.sml | 300 mk_sums Arbnum.zero 357 mk_c Arbnum.zero (BCARRY_def |> Thm.CONJUNCT1 |> Drule.SPECL [x,y,c]) 555 handle HOL_ERR _ => (Arbnum.zero, Arbnum.zero) 557 if sz = Arbnum.zero orelse Arbnum.< (n, Arbnum.fromInt 11) 1089 bit_theorem Arbnum.zero []
|
/seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
H A D | bvec.c | 209 vector will have the LSB at position zero. *} 289 DESCR {* Returns non-zero if the vector {\tt v} consists of only constant 290 true or false BDDs. Otherwise zero is returned. This test should 313 or false BDDs. The LSB is assumed to be at position zero. *} 752 bvec zero = bvec_build(divisor.bitnum, bddfalse); local 756 sub.bitvec[n] = bdd_ite(isSmaller, divisor.bitvec[n], zero.bitvec[n]); 766 bvec_free(zero);
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | threads.tex | 169 a label of zero, the thread will be restarted. Additionally, if the 170 message length is non-zero, the faulting thread's register set will be 179 divide a number by zero. 183 a label of zero, the thread will be restarted. Additionally, if the 184 message length is non-zero, the faulting thread's register set will be 297 should be set to \texttt{1} when single-stepping, or any non-zero integer value to skip that many
|
/seL4-l4v-10.1.1/HOL4/src/patricia/ |
H A D | patriciaLib.sml | 45 fun even n = Arbnum.mod2 n = Arbnum.zero 50 if x = 0 orelse n = Arbnum.zero 51 then Arbnum.zero 64 fun lt_2exp x n = x = Arbnum.zero orelse Arbnum.toInt (Arbnum.log2 x) < n 182 fun l2n [] = Arbnum.zero
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | EnumType.sml | 56 (* thm of form x < n, where n is a non-zero numeral *) 73 (* nlt_thm is of the form |- n < x where x is non-zero *) 132 Make a size definition for an enumerated type (everywhere zero)
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Norm_arith.sml | 165 in if (aval = zero) then SPEC b ZERO_MULT 167 else if (bval = zero) then SPEC a MULT_ZERO
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | combin.tex | 167 il secondo pu� essere raggiunto dal primo in zero o pi� passi. Questa 177 con zero o pi� ``passi'' della relazione $R$. (La notazione 180 che � sempre possibile andare da $x$ a $x$ in zero o pi� 184 zero o pi� passi per andare da $y$ a $z$, allora � possibile fare 185 zero o pi� passi per andare da $x$ a $z$. La realizzazione di 318 Cos�, da $y$ possiamo fare zero o pi� passi per arrivare a $u$ e 494 un passo verso $z$, e abbiamo bisogno di trovare un qualche posto raggiungibile in zero o 671 $y$ sia $v$ si possono connettere in zero o pi� passi, ma al fine di
|
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
H A D | jedit_editor.scala | 251 (Line.Position.zero /:
|