| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | cacheTools.sml | 702 val abs = frv_insert(abs,lhs(concl (xabthm)),xabthm) value
718 val abs = frv_insert(frv_merge absl absr,lhs(concl (xabthm)),xabthm) value
735 val abs = frv_insert(frv_merge absl absr,lhs(concl (xabthm)),xabthm) value
746 val abs value
757 val abs = frv_insert(abs,lhs(concl (xabthm)),xabthm) value
770 val abs = frv_insert(abs,List.last args,xabthm) value
783 val abs = frv_insert(abs,lhs(concl (xabthm)),xabthm) value
797 val abs = frv_insert(abs,List.last args,xabthm) value
814 val abs = frv_insert(abs,lhs(concl (xabthm)),xabthm) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
| H A D | circuits.lisp | [all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/lib/ |
| 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 | FP.sml | 13 val abs: BitsN.nbit -> BitsN.nbit value
|
| H A D | FP32.sml | 33 fun abs _ = err "abs" function
|
| H A D | FP64.sml | 95 val abs = fpOp0 R.abs value
|
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| 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 | Int32.sml | 55 val abs = check o abs value
|
| H A D | OS.sml | 397 val {abs = nowAbs, ...} = matchVolumePrefix r value
[all...] |
| H A D | RealSignature.sml | 45 val abs : real -> real value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | Ho_Rewrite.sml | 235 val abs = mk_abs(gv,subst[stm |-> gv] tm) value
|
| H A D | selftest.sml | 250 val abs = mk_abs(n, mk_comb(FST, mk_comb(f',n))) value
|
| /seL4-l4v-10.1.1/HOL4/src/bool/ |
| H A D | boolScript.sml | 453 val abs = MP (FALSITY_CONV (F == T)) (MP (ASSUME (T ==> F)) TRUTH) value
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/ |
| H A D | EnumType.sml | 351 val abs = "num2" ^ ty value
|
| H A D | ind_types.sml | 120 val abs = list_mk_abs(gvs,pat) value
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/equiv/ |
| H A D | EquivType.sml | 103 val (abs,rep) = ((I ## rator) o dest_comb o lhs o snd o dest_forall value
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
| H A D | MutRecDef.sml | 497 val abs = mk_const{Name = abs_name, value
1161 val {abs value
1356 val abs = mk_comb{Rator = get_abs type_name, Rand = Joint_x} value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibArbint.sig | 39 val abs : int -> int value
|
| H A D | mlibArbint.sml | 119 fun abs (_, n) = (true, n) function
|
| H A D | mlibOmegaint.sig | 33 val abs : int -> int value
|
| /seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
| H A D | NDatatype.sml | 429 val abs = map snd repabss value
|
| /seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/ |
| H A D | Logging.sml | 347 val abs = mk_var("abs",alpha-->beta) value
549 val abs = rand(concl th) value
582 val abs = rand(concl th1) value
654 val abs = prim_new_const abstc absty value
[all...] |
| H A D | Opentheory.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...] |