| /seL4-l4v-master/HOL4/examples/HolCheck/ |
| H A D | lzPairRules.sml | 185 val arg = (list_mk_pair(List.map (fn k => Binarymap.find(sbm,k)) (strip_pair bp))) value
|
| /seL4-l4v-master/HOL4/examples/acl2/ml/ |
| H A D | functionEncodeLib.sml | 2095 val arg = variant vars (mk_var("arg",t)) value
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/ |
| H A D | compile.sml | 1582 then let val arg = rand bdy value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | mechReasoning.sml | |
| /seL4-l4v-master/HOL4/examples/dev/sw2/ |
| H A D | defunctionalize.sml | 286 val arg = mk_pair(clos_arg, f_arg) value
334 val (arg, body) = dest_pabs M value
|
| H A D | monomorphisation.sml | 184 val (arg, body) = dest_pabs M value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/ |
| H A D | arm.sml | 25537 val arg = (single,(add,(d,(n,imm32)))) value
25548 val arg = value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/ |
| H A D | x64.sml | 4110 val arg = (size,(Zr_rm(reg,rm),size2)) value
5891 val arg = (sz,(rm,r)) value
|
| /seL4-l4v-master/HOL4/examples/machine-code/graph/ |
| H A D | exportLib.sml | 212 fun arg s = "" ^ s ^ " " ^ get_var_type s function
|
| /seL4-l4v-master/HOL4/examples/separationLogic/src/ |
| H A D | separationLogicSyntax.sml | 177 val arg = strip_comb_1 COND_PROP___STRONG_EXISTS_term tt; value
189 val arg = strip_comb_1 COND_PROP___EXISTS_term tt; value
243 val arg = strip_comb_1 asl_exists_term tt; value
|
| /seL4-l4v-master/HOL4/polyml/libpolyml/ |
| H A D | mpoly.cpp | 162 POLYUNSIGNED parseSize(const TCHAR *p, const TCHAR *arg) argument
|
| /seL4-l4v-master/HOL4/src/1/ |
| H A D | BoundedRewrites.sml | 18 val arg = rand h value
|
| H A D | Prim_rec.sml | 362 val arg = rand lhs value
|
| /seL4-l4v-master/HOL4/src/integer/ |
| H A D | CooperMath.sml | 104 val arg = term_at dir tm value
795 val arg = hd (tl args) (* first arg is uninteresting, it should be value
924 val arg = mk_mult(term_of_int lcm, var) value
|
| /seL4-l4v-master/HOL4/src/list/src/ |
| H A D | ListConv1.sml | 640 val arg = dest_flat t value
|
| /seL4-l4v-master/HOL4/src/parse/ |
| H A D | ParseDatatype.sml | 286 val arg = parse_harg G qb value
|
| H A D | Parse_support.sml | |
| /seL4-l4v-master/HOL4/src/pattern_matches/ |
| H A D | constrFamiliesLib.sml | 848 val arg = mk_comb (split_fun, split_arg) value
|
| /seL4-l4v-master/HOL4/src/proofman/ |
| H A D | goalStack.sml | 171 let val arg = (case stack of [] => g | tr::_ => hd (#goals tr)) value
|
| /seL4-l4v-master/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsLibBase.sml | 2980 let val arg = (combine_qps (bqp::args)) in value
3062 let val arg = (combine_qps (bqp::args)) in value
3067 let val arg = (combine_qps (bqp::args)) in value
[all...] |
| /seL4-l4v-master/HOL4/src/real/ |
| H A D | Diff.sml | 94 let val arg = Lib.trye hd args value
|
| /seL4-l4v-master/HOL4/tools/mlyacc/mlyacclib/ |
| H A D | MLY_base-sig.sml | 181 type arg type
207 type arg type
272 type arg type
308 type arg type
[all...] |
| H A D | MLY_join.sml | 44 type arg = ParserData.arg type
88 type arg = ParserData.arg type
[all...] |
| /seL4-l4v-master/HOL4/tools/mlyacc/src/ |
| H A D | yacc-grm.sml | 308 type arg = Hdr.inputSource type
|
| /seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
| H A D | base.sig | 157 type arg type
183 type arg type
248 type arg type
284 type arg type
[all...] |