Searched defs:mk_less (Results 1 - 9 of 9) sorted by relevance

/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.sml64 val mk_less = numSyntax.mk_less value
/seL4-l4v-10.1.1/HOL4/src/real/
H A DrealSyntax.sig65 val mk_less : (term * term) -> term value
H A DrealSyntax.sml143 fun mk_less(t1, t2) = list_mk_comb(less_tm, [t1, t2]) function
/seL4-l4v-10.1.1/HOL4/src/integer/
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
/seL4-l4v-10.1.1/HOL4/src/num/theories/
H A DnumSyntax.sig51 val mk_less : term * term -> term value
H A DnumSyntax.sml63 val mk_less = mk_binop less_tm value
/seL4-l4v-10.1.1/graph-refine/
H A Dsyntax.py1356 def mk_less (x, y, signed = False): function

Completed in 78 milliseconds