| /seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/ |
| H A D | completion_popup.scala | 357 if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
524 if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/ |
| H A D | completion_popup.scala | 357 if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
524 if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
| H A D | markup.scala | 391 (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
| H A D | markup.scala | 391 (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
|
| /seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
| H A D | timing.scala | 42 def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
|
| H A D | time.scala | 51 def is_zero: Boolean = ms == 0
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
| H A D | timing.scala | 42 def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
|
| H A D | time.scala | 51 def is_zero: Boolean = ms == 0
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | loop_bounds.py | 234 def is_zero (expr): function
246 if is_zero (x) and y.is_op ('Plus'):
250 elif is_zero (x) and y.is_op ('Minus'):
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | Literal.sig | 6 val is_zero : term -> bool value
|
| H A D | Literal.sml | 107 val is_zero = Lib.can dest_zero; value
243 is_literal x andalso not (is_zero x) andalso not (is_string_lit x);
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | Term_coeffs.sml | 236 if is_zero rest then prod else mk_plus (prod,rest)
243 if is_zero rest then c
|
| H A D | Norm_arith.sml | 265 in if (is_zero tm1) then (SPEC tm2 ZERO_MULT)
266 else if (is_zero tm2) then (SPEC tm1 MULT_ZERO)
309 in if (is_zero tm1) then (SPEC tm2 ZERO_PLUS)
310 else if (is_zero tm2) then (SPEC tm1 PLUS_ZERO)
|
| H A D | Gen_arith.sml | 42 (if (is_zero tm) then failwith "fail" else not (is_num_const tm))
|
| H A D | Arith_cons.sig | 36 val is_zero : term -> bool value
|
| H A D | Arith_cons.sml | 109 fun is_zero tm = (tm = zero) function
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | wordsLib.sml | 944 fun is_zero tm = function
974 if is_zero l
979 | _ => if is_zero tm
1029 val l = if is_zero l then [] else get_coeff_terms [] l
1030 val r = if is_zero r then [] else get_coeff_terms [] r
|
| /seL4-l4v-10.1.1/HOL4/src/float/ |
| H A D | ieeeScript.sml | 109 val is_zero = new_definition ( value
110 "is_zero",
111 ���is_zero (X:num#num) (a:num#num#num) = ((exponent a = 0) /\ (fraction a = 0))���);
125 ((is_valid (X) a) /\ ((is_normal(X:num#num) a) \/ (is_denormal(X:num#num) a) \/ (is_zero (X:num#num) a)))���);
298 ���zerosign (X:num#num) (s:num) (a:num#num#num) = (if (is_zero(X) a) then
326 else zerosign(X) (if is_zero(X) a /\ is_zero(X) b /\ (sign(a) = sign(b)) then sign(a) else if (m = To_ninfinity) then 1 else 0) (round(X) m (valof(X) a + valof(X) b))���);
334 else zerosign(X) (if is_zero(X) a /\ is_zero(X) b /\ ~(sign(a) = sign(b)) then sign(a) else if m = To_ninfinity then 1 else 0) (round(X) m (valof(X) a - valof(X) b)))���);
339 (if is_nan(X) a \/ is_nan(X) b \/ is_zero(
[all...] |
| H A D | floatScript.sml | 84 \\ simp [is_valid, is_finite, is_normal, is_denormal, is_zero, exponent, emax,
95 is_nan, is_infinity, is_normal, is_denormal, is_zero, IS_VALID, emax]
116 is_nan, is_infinity, is_normal, is_denormal, is_zero,
155 \\ fs [Iszero, Plus_zero, Minus_zero, is_zero, plus_zero, minus_zero,
355 \\ rw [is_finite, is_valid, is_zero, exponent, fraction]
404 \\ fs [is_zero, exponent, fraction, valof]
1168 \\ simp [Finite, Iszero, is_zero, exponent, fraction, Val, valof]
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Pmatch.sml | 234 Literal.is_zero tm orelse Literal.is_emptystring tm orelse is_var tm
|
| /seL4-l4v-10.1.1/HOL4/examples/computability/lambda/ |
| H A D | churchnumScript.sml | 369 (* $< 0 = ��n. not (is_zero n)
370 $< (SUC m) = ��n. not (is_zero n) ��� $< m (PRE n)
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | arm_parserLib.sml | 531 fun is_zero x = x = Arbnum.zero function
534 case (is_zero b3, is_zero b2, is_zero b1, is_zero b0)
|