| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | Arith_cons.sml | 61 (* mk_less, mk_leq, mk_great, mk_geq *)
64 val mk_less = numSyntax.mk_less value
|
| H A D | Arith_cons.sig | 16 val mk_less : term * term -> term value
|
| /seL4-l4v-10.1.1/HOL4/src/integer/testing/ |
| H A D | gen_bc_problem.sml | 21 val opn = if r < 0.33 then mk_eq else mk_less
|
| H A D | genproblem.sml | 22 else if r < 0.4 then mk_less(gen_term(), gen_term())
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | SmtLib_Theories.sml | 268 ("<", chainable intSyntax.mk_less),
299 ("<", chainable realSyntax.mk_less),
330 ("<", chainable intSyntax.mk_less),
341 ("<", chainable realSyntax.mk_less),
|
| H A D | SmtLib_Logics.sml | 123 ("<", chainable (realSyntax.mk_less o one_int_to_real)),
|
| /seL4-l4v-10.1.1/HOL4/src/real/ |
| H A D | realSyntax.sig | 65 val mk_less : (term * term) -> term value
|
| H A D | realSyntax.sml | 143 fun mk_less(t1, t2) = list_mk_comb(less_tm, [t1, t2]) function
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | intSyntax.sig | 91 val mk_less : (term * term) -> term value
|
| H A D | OmegaSimple.sml | 132 val zero_lt_c = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, c)))
165 (EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, d_t))))
|
| H A D | CooperCore.sml | 158 val MK_LESS = if use_bis then mk_less else (fn (x,y) => mk_less(y,x))
291 val restriction = mk_conj(mk_less(zero_tm, i),
317 val jrestriction = mk_conj(mk_less(zero_tm, j), mk_leq(j, delta_tm))
359 val zero_lt_delta = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, delta_tm)))
362 EQT_ELIM (REDUCE_CONV (mk_conj(mk_less(zero_tm, one_tm),
|
| H A D | intSyntax.sml | 135 fun mk_less (tm1, tm2) = list_mk_comb(less_tm, [tm1, tm2]) function
|
| H A D | jrhCore.sml | 106 val zero_lt_lcm = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, lcm_t)))
|
| /seL4-l4v-10.1.1/HOL4/src/floating-point/ |
| H A D | binary_ieeeLib.sml | 318 fun mk_abs_diff_lt (x, r, u) = realSyntax.mk_less (mk_abs_diff (x, r), u)
322 fun mk_abs_lt (r, x) = realSyntax.mk_less (cond_mk_absval true r, x)
434 (realSyntax.mk_less
527 realSyntax.mk_less (x, mk_neg_large tw)
535 val lt = realSyntax.mk_less (mk_large tw, x)
551 val lt = realSyntax.mk_less (mk_large tw, x)
568 val lt = realSyntax.mk_less (x, mk_neg_large tw)
|
| /seL4-l4v-10.1.1/HOL4/src/num/theories/ |
| H A D | numSyntax.sig | 51 val mk_less : term * term -> term value
|
| H A D | numSyntax.sml | 63 val mk_less = mk_binop less_tm value
|
| /seL4-l4v-10.1.1/HOL4/src/string/ |
| H A D | stringLib.sml | 17 Drule.EQT_ELIM (reduceLib.LT_CONV (numSyntax.mk_less (m, bound)))
|
| H A D | stringScript.sml | 30 in mk_abs(n,mk_less(n,topnum))
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | logic.py | 15 mk_less_eq, mk_less, mk_implies, mk_and, mk_or, mk_not, mk_word32, mk_word8,
164 preconds += [mk_less (last_arg_addr, addr)
461 out1 = mk_less (end_addr (p, typ), p2)
462 out2 = mk_less (end_addr (p2, typ2), p)
482 out1 = mk_less (mk_plus (p, mk_word32 (typ.size () - 1)), mk_word32 (start))
483 out2 = mk_less (mk_word32 (end), p)
556 return lambda offs: mk_and (mk_less (offs, size),
612 mk_implies (mk_less (w0, size),
|
| H A D | loop_bounds.py | 267 fin_cmp1 = syntax.mk_less (x, y)
268 fin_cmp2 = syntax.mk_less (y, x)
|
| /seL4-l4v-10.1.1/HOL4/src/num/ |
| H A D | numLib.sml | 235 (EQT_ELIM(REDUCE_CONV (mk_less(zero_tm,c))))
256 (EQT_ELIM(REDUCE_CONV (mk_less(zero_tm,c))))
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/ |
| H A D | EnumType.sml | 23 in mk_abs(n,mk_less(n,topnum))
37 val less_thm = EQT_ELIM (REDUCE_CONV (mk_less(n,top_numeral)))
278 mk_cond(mk_less(m, mk_numeral (Arbnum.fromInt mid)),
|
| /seL4-l4v-10.1.1/HOL4/src/num/reduce/src/ |
| H A D | Arithconv.sml | 220 fun provelt x y = EQT_ELIM (LT_CONV (mk_less(mk_numeral x, mk_numeral y)))
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | wordsLib.sml | 686 val lt_thm = numSyntax.mk_less (n, wordsSyntax.mk_dimindex ty)
727 val lt_thm = numSyntax.mk_less (n, dim_sub1)
1817 |> numSyntax.mk_less
1847 (numLib.DECIDE (numSyntax.mk_less (numSyntax.zero_tm, n)))]
1911 val l_lt = numSyntax.mk_less (l, sz)
1912 val r_lt = numSyntax.mk_less (r, sz)
2400 numSyntax.mk_less (numSyntax.zero_tm, n)
2402 fun thm4 () = numSyntax.mk_less (n,
|
| H A D | bitstringLib.sml | 330 numSyntax.mk_less (i, fcpSyntax.mk_dimindex ty)
|