| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibOmegaint.sig | 33 val abs : int -> int value
|
| H A D | mlibArbint.sig | 39 val abs : int -> int value
|
| H A D | mlibArbint.sml | 119 fun abs (_, n) = (true, n) function
|
| /seL4-l4v-master/HOL4/polyml/basis/ |
| H A D | Int32.sml | 55 val abs = check o abs value
|
| H A D | INTEGER.sml | 46 val abs : int -> int value
|
| H A D | Int.sml | 49 val abs : int -> int value
82 fun abs (i: int): int = if i >= zero then i else ~ i function
|
| H A D | RealSignature.sml | 45 val abs : real -> real value
|
| /seL4-l4v-master/HOL4/src/portableML/ |
| H A D | Arbrat.sig | 33 val abs : rat -> rat value
|
| H A D | Arbrat.sml | 62 fun abs(n, d) = (Arbint.abs n, d) function
|
| /seL4-l4v-master/HOL4/src/portableML/mosml/ |
| H A D | Arbintcore.sig | 31 val abs : int -> int value
|
| H A D | Arbintcore.sml | 119 fun abs (_, n) = (true, n) function
|
| /seL4-l4v-master/HOL4/src/portableML/poly/ |
| H A D | Arbintcore.sig | 33 val abs : int -> int value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/lib/ |
| H A D | FP.sml | 13 val abs: BitsN.nbit -> BitsN.nbit value
|
| H A D | FP32.sml | 33 fun abs _ = err "abs" function
|
| H A D | BitsN.sig | 66 val abs: nbit -> nbit value
|
| H A D | BitsN.sml | 251 fun abs a = if msb a then neg a else a function
|
| H A D | FP64.sml | 95 val abs = fpOp0 R.abs value
|
| /seL4-l4v-master/HOL4/src/opentheory/reader/ |
| H A D | OpenTheoryReader.sml | 187 val (abs,foo) = dest_comb(#2(dest_abs(lhs(concl abs_rep)))) value
190 val {Thy,Name,...} = dest_thy_const abs va value
[all...] |
| /seL4-l4v-master/HOL4/src/real/ |
| H A D | prove_real_assumsScript.sml | 69 val abs = ``real_ABS`` value
|
| /seL4-l4v-master/HOL4/examples/acl2/tests/inputs/ |
| H A D | circuits.lisp | [all...] |
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | Ho_Rewrite.sml | 235 val abs = mk_abs(gv,subst[stm |-> gv] tm) value
|
| /seL4-l4v-master/HOL4/src/rational/ |
| H A D | fracLib.sml | 208 val (abs,args) = dest_comb f; value
227 val (abs,args) = dest_comb f; value
|
| H A D | fracScript.sml | 290 val (abs,args) = dest_comb f; value
309 val (abs,args) = dest_comb f; value
|
| /seL4-l4v-master/HOL4/src/new-datatype/ |
| H A D | NDatatype.sml | 428 val abs = map snd repabss value
|
| /seL4-l4v-master/HOL4/tools/Holmake/ |
| H A D | Holmake_tools.sml | 507 val abs = toAbsPath d value
|