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

/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DArith_cons.sig7 val mk_plus : term * term -> term value
H A DArith_cons.sml36 val mk_plus = numSyntax.mk_plus value
/seL4-l4v-10.1.1/HOL4/src/real/
H A DrealSyntax.sig40 val mk_plus : (term * term) -> term value
H A DrealSyntax.sml88 fun mk_plus(t1, t2) = list_mk_comb(plus_tm, [t1, t2]) function
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DintSyntax.sig50 val mk_plus : (term * term) -> term value
H A DintSyntax.sml46 fun mk_plus (arg1, arg2) = list_mk_comb(plus_tm, [arg1, arg2]) function
/seL4-l4v-10.1.1/HOL4/src/num/theories/
H A DnumSyntax.sig60 val mk_plus : term * term -> term value
H A DnumSyntax.sml70 val mk_plus = mk_binop plus_tm value
/seL4-l4v-10.1.1/graph-refine/
H A Dsyntax.py1318 def mk_plus (x, y): function

Completed in 67 milliseconds