| /seL4-l4v-10.1.1/HOL4/src/real/ |
| H A D | realSimps.sml | 318 if n_i = zero then REWR_CONV REAL_DIV_LZERO t
321 val _ = d_i > zero orelse
|
| /seL4-l4v-10.1.1/HOL4/examples/CCS/ |
| H A D | ObsCongrScript.sml | 577 (* `EPS E E1` implies zero or more tau transitions, and this leads to
578 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_FUNCTIONS.sml | 133 | WordArith _ => applicative (* Quot and Rem don't raise exceptions - zero checking is done before. *)
139 | LargeWordArith _ => applicative (* Quot and Rem don't raise exceptions - zero checking is done before. *)
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
| H A D | markup.scala | 396 val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
| H A D | markup.scala | 396 val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | mechReasoning.sml | 100 val _ = if (r = Arbnum.zero) then () else Raise (ERR "" "Syntax");
1056 if (n2 = Arbnum.zero) then
1064 if (n = Arbnum.zero) then
1068 val (n_div, n_mod) = remove_zero n Arbnum.zero;
|
| H A D | IR.sml | 185 Tree.NCONST Arbint.zero
|
| H A D | IRSyntax.sml | 159 fun smsb b = if b then Arbnum.pow(Arbnum.two,Arbnum.fromInt 31) else Arbnum.zero
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | IR.sml | 185 Tree.NCONST Arbint.zero
|
| H A D | IRSyntax.sml | 159 fun smsb b = if b then Arbnum.pow(Arbnum.two,Arbnum.fromInt 31) else Arbnum.zero
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Thm_cont.sml | 267 * where the xl1...xln are vectors of zero or more variables, and the
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | OmegaSimple.sml | 10 With each c_i and the n an integer literal. The n may be zero, but
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | parse_type.sml | 99 val _ = n <> Arbnum.zero orelse
|
| /seL4-l4v-10.1.1/HOL4/src/prekernel/ |
| H A D | Lexis.sml | 32 * zero, bone is the representation of one.
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
| H A D | armParser.lex | 83 "+"?0 => ( Tokens.NUMBER (Arbnum.zero, !pos, !pos) );
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
| H A D | CommonDialog.sml | 1157 (* Since we're not going to set all of it we need to zero it. *)
1159 fun zero n = if n = printDlgSize then () else (set8(mem, n, 0w0); zero(n+0w1)) function
1161 val () = zero 0w0
|
| H A D | DeviceBase.sml | 452 (* Optional values default to zero. If the option is SOME v we set the
|
| /seL4-l4v-10.1.1/isabelle/src/Doc/Logics/document/ |
| H A D | Sequents.tex | 27 is intended to match a sequence of zero or more items.
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Logics/document/ |
| H A D | Sequents.tex | 27 is intended to match a sequence of zero or more items.
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/Tools/ |
| H A D | build.scala | 324 if (info.timeout > Time.zero)
835 (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
| H A D | build.scala | 324 if (info.timeout > Time.zero)
835 (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
|
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | tutorial.ml | 186 (* argument is non-zero. The propagation theorems are as follows: *)
198 (* arguments are non-zero: *)
425 (* function determining whether all elements are non-zero: *)
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | solver.py | 494 zero = '#x00000000'
496 (x_split, x_top, x_bot) = (zero, x, x)
500 (y_split, y_top, y_bot) = (zero, y, y)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | IRSyntax.sml | 159 fun smsb b = if b then Arbnum.pow(Arbnum.two,Arbnum.fromInt 31) else Arbnum.zero
|
| H A D | mechReasoning.sml | 141 val _ = if (r = Arbnum.zero) then () else Raise (ERR "" "Syntax");
1608 if (n2 = Arbnum.zero) then
1616 if (n = Arbnum.zero) then
1620 val (n_div, n_mod) = remove_zero n Arbnum.zero;
|