| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | arm_parserLib.sml | 1762 val offset = eval (mk_minus(i, ``8i``))
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | Import.sml | 1182 SOME numSyntax.mk_minus, SOME intSyntax.mk_minus)
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/step/ |
| H A D | x64_stepLib.sml | 1108 (numSyntax.mk_minus (twenty, listSyntax.mk_length (get_strm1 thm1)))
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootLib.sml | 587 numSyntax.mk_minus (numSyntax.mk_suc c2, c1))
|
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | SmtLib_Logics.sml | 118 ("-", leftassoc (realSyntax.mk_minus o one_int_to_real)),
|
| H A D | SmtLib_Theories.sml | 262 ("-", leftassoc intSyntax.mk_minus),
294 ("-", leftassoc realSyntax.mk_minus),
324 ("-", leftassoc intSyntax.mk_minus),
336 ("-", leftassoc realSyntax.mk_minus),
|
| /seL4-l4v-10.1.1/HOL4/src/floating-point/ |
| H A D | binary_ieeeLib.sml | 317 fun mk_abs_diff (x, r) = realSyntax.mk_absval (realSyntax.mk_minus (x, r))
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | CooperCore.sml | 245 if use_bis then (mk_comb (neginf, mk_minus(Bvar, mk_mult(y, delta_tm))),
311 else (find_ai, mk_minus)
1010 if use_bis then (mk_minus, brecurse) else (mk_plus, arecurse)
|
| H A D | intSyntax.sig | 57 val mk_minus : (term * term) -> term value
|
| H A D | intSyntax.sml | 68 fun mk_minus (tm1, tm2) = list_mk_comb(minus_tm, [tm1, tm2]) function
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | bitstringLib.sml | 278 boolSyntax.mk_eq (dim_b, numSyntax.mk_minus (numSyntax.mk_suc h, l))
|
| H A D | wordsLib.sml | 726 numSyntax.mk_minus (wordsSyntax.mk_dimindex ty, one_tm)
1597 numSyntax.mk_minus (numSyntax.mk_plus (h, ``1n``), l))
|
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | Arith_cons.sig | 8 val mk_minus : term * term -> term value
|
| H A D | Arith_cons.sml | 33 (* mk_plus, mk_minus, mk_mult *)
37 and mk_minus = numSyntax.mk_minus value
|
| H A D | numSimps.sml | 205 else mk_minus(x,list_mk_plus neg_terms)
207 else mk_minus(list_mk_plus (pos_terms@[x]),
214 else mk_minus(list_mk_plus pos_terms,list_mk_plus neg_terms)
|
| /seL4-l4v-10.1.1/HOL4/src/num/theories/ |
| H A D | numSyntax.sig | 55 val mk_minus : term * term -> term value
|
| H A D | numSyntax.sml | 66 val mk_minus = mk_binop minus_tm value
|
| /seL4-l4v-10.1.1/HOL4/src/real/ |
| H A D | realSyntax.sig | 47 val mk_minus : (term * term) -> term value
|
| H A D | realSyntax.sml | 109 fun mk_minus(t1,t2) = list_mk_comb(minus_tm, [t1, t2]) function
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | check.py | 24 mk_plus, mk_minus, word32T, word8T, mk_and, mk_eq, mk_implies, mk_not,
|
| H A D | logic.py | 14 (mk_var, mk_plus, mk_uminus, mk_minus, mk_times, mk_modulus, mk_bwand, mk_eq,
307 (x, i, mk_minus (x, y), mk_minus (x, mk_times (i, y)),
321 (x, i, mk_minus (mk_minus (x, y), z),
322 mk_minus (x, mk_times (i, mk_plus (y, z))),
402 return mk_minus (vals[0], vals[1])
448 return mk_plus (p, mk_minus (sz, mk_word32 (1)))
456 offs1 = mk_minus (p, p2)
458 offs2 = mk_minus (p
[all...] |
| H A D | pseudo_compile.py | 16 (mk_var, mk_plus, mk_uminus, mk_minus, mk_times, mk_modulus, mk_bwand, mk_eq,
|
| H A D | search.py | 19 mk_num, mk_minus, mk_plus, mk_less)
935 get_int_min (mk_minus (expr_init, smt (expr, n, 0))),
|
| H A D | stack_logic.py | 363 ps = [(syntax.mk_minus (p, syntax.mk_word32 (n)), n)
|
| H A D | syntax.py | 1324 return mk_minus (zero, x)
1326 def mk_minus (x, y): function
1485 mks = (mk_var, mk_plus, mk_uminus, mk_minus, mk_times, mk_modulus, mk_bwand,
|