| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | Holmake_tools.sml | 458 val abs = toAbsPath d value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| 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/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/quotient/examples/sigma/ |
| H A D | liftScript.sml | [all...] |
| /seL4-l4v-10.1.1/HOL4/src/refute/ |
| H A D | Canon.sml | 638 val abs = mk_abs(gv,subst[t |-> gv] tm) value
|
| /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/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/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...] |
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | OS.sml | 397 val {abs = nowAbs, ...} = matchVolumePrefix r value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/quotient/src/ |
| H A D | quotient.sml | 658 val abs = el 2 R_abs_rep value
1359 val abs = (hd o tl) args value
1582 val abs = (hd o tl) Rar value
1674 val abs = hd (tl Rar) value
2143 val abs = hd (tl Rar) value
3564 val abs = mk_set (findabs tm) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/real/ |
| H A D | RealArith.sml | 1006 fun abs x = if x < zero then ~x else x; function
[all...] |
| H A D | realScript.sml | 1367 val abs = new_definition("abs", value
[all...] |
| /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
|