Searched refs:mk_less (Results 1 - 25 of 37) sorted by path

12

/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DImport.sml1169 SOME numSyntax.mk_less, SOME intSyntax.mk_less)
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A DholfootLib.sml229 numSyntax.mk_less (ec, numSyntax.mk_plus (ec', nc')))
2228 if i2 then (SOME (mk_disj (numSyntax.mk_less (nc2, ec1), mk_eq (ec2, ec1))),
/seL4-l4v-10.1.1/HOL4/src/HolSmt/
H A DSmtLib_Logics.sml123 ("<", chainable (realSyntax.mk_less o one_int_to_real)),
H A DSmtLib_Theories.sml268 ("<", chainable intSyntax.mk_less),
299 ("<", chainable realSyntax.mk_less),
330 ("<", chainable intSyntax.mk_less),
341 ("<", chainable realSyntax.mk_less),
/seL4-l4v-10.1.1/HOL4/src/datatype/
H A DEnumType.sml23 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/floating-point/
H A Dbinary_ieeeLib.sml318 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/integer/
H A DCooperCore.sml158 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 DCooperMath.sml317 val g_t_lt0 = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, g_t)))
918 EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, term_of_int i)))
H A DIntDP_Munge.sml287 val div_nzero = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, divisor)))
H A DOmegaMath.sml126 val zero_lt_g = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, g_t)))
H A DOmegaSimple.sml132 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 DOmegaSymbolic.sml293 EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, f)))
H A DintSyntax.sig91 val mk_less : (term * term) -> term value
H A DintSyntax.sml135 fun mk_less (tm1, tm2) = list_mk_comb(less_tm, [tm1, tm2]) function
H A DjrhCore.sml106 val zero_lt_lcm = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, lcm_t)))
/seL4-l4v-10.1.1/HOL4/src/integer/testing/
H A Dgen_bc_problem.sml21 val opn = if r < 0.33 then mk_eq else mk_less
H A Dgenproblem.sml22 else if r < 0.4 then mk_less(gen_term(), gen_term())
/seL4-l4v-10.1.1/HOL4/src/n-bit/
H A DbitstringLib.sml330 numSyntax.mk_less (i, fcpSyntax.mk_dimindex ty)
H A DblastLib.sml43 numSyntax.mk_less (i, j)
124 val thm = numSyntax.mk_less (ti, lvs)
H A DwordsLib.sml686 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,
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DArith_cons.sig16 val mk_less : term * term -> term value
H A DArith_cons.sml61 (* mk_less, mk_leq, mk_great, mk_geq *)
64 val mk_less = numSyntax.mk_less value
H A DnumSimps.sml560 mDISCH (mk_less(zero_tm, v)) (REWRITE_RULE [base_rewrite] base_thm)
/seL4-l4v-10.1.1/HOL4/src/num/
H A DnumLib.sml235 (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/num/reduce/src/
H A DArithconv.sml220 fun provelt x y = EQT_ELIM (LT_CONV (mk_less(mk_numeral x, mk_numeral y)))

Completed in 158 milliseconds

12