/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
H A D | Import.sml | 1169 SOME numSyntax.mk_less, SOME intSyntax.mk_less)
|
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootLib.sml | 229 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 D | SmtLib_Logics.sml | 123 ("<", chainable (realSyntax.mk_less o one_int_to_real)),
|
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),
|
/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/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/integer/ |
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 | CooperMath.sml | 317 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 D | IntDP_Munge.sml | 287 val div_nzero = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, divisor)))
|
H A D | OmegaMath.sml | 126 val zero_lt_g = EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, g_t)))
|
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 | OmegaSymbolic.sml | 293 EQT_ELIM (REDUCE_CONV (mk_less(zero_tm, f)))
|
H A D | intSyntax.sig | 91 val mk_less : (term * term) -> term value
|
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/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/n-bit/ |
H A D | bitstringLib.sml | 330 numSyntax.mk_less (i, fcpSyntax.mk_dimindex ty)
|
H A D | blastLib.sml | 43 numSyntax.mk_less (i, j) 124 val thm = numSyntax.mk_less (ti, lvs)
|
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,
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Arith_cons.sig | 16 val mk_less : term * term -> term value
|
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 | numSimps.sml | 560 mDISCH (mk_less(zero_tm, v)) (REWRITE_RULE [base_rewrite] base_thm)
|
/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/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)))
|