/seL4-l4v-master/HOL4/src/1/ |
H A D | Rsyntax.sml | 23 fun mk_let{func,arg} = boolSyntax.mk_let(func,arg) 50 fun dest_let M = let val (f,a) = boolSyntax.dest_let M in {func=f,arg=a} end;
|
H A D | Rsyntax.sig | 22 val mk_let : {arg:term, func:term} -> term 39 val dest_let : term -> {arg:term, func:term}
|
/seL4-l4v-master/HOL4/src/bag/ |
H A D | bagSyntax.sml | 98 val (f, arg) = dest_comb tm 102 arg 110 val (f, arg) = dest_comb tm 114 arg
|
/seL4-l4v-master/HOL4/tools/mlyacc/src/ |
H A D | parse.sml | 28 sharing type Parser.arg = Header.inputSource =
|
/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttTrain.sml | 152 fun nntm_of_arg arg = case arg of 156 fun nntm_of_statearg ((g,stac),arg) = 158 mk_binop gstacarg_cat (nntm_of_gstac (g,stac), nntm_of_arg arg))
|
/seL4-l4v-master/HOL4/src/coretypes/ |
H A D | PairedLambda.sml | 91 let val (abst,arg) = dest_comb tm 95 val eqv = if can dest_pair arg then REFL arg else ISPEC arg pair 254 val (func, arg) = boolSyntax.dest_let tm 257 val thm = RIGHT_BETA (AP_THM (RIGHT_BETA (AP_THM defn func)) arg) 260 then REDUCE func arg (RIGHT_BETA thm) 266 (AP_TERM (rator (rator tm)) (conv bconv func)) arg)
|
H A D | pairLib.sml | 20 (* given (��(x,y,...) ...) arg (UOK) 22 arg = (x,y,...) 31 (* ?x y z ... . arg = (x,y,z,...) *)
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | Lexer.lex | 2 type arg = int; 182 %arg (commentDepth);
|
/seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | parser1.sml | 44 val parse = fn {arg : 'a, 83 saction(i,leftPos,stack,arg)
|
/seL4-l4v-master/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | parser1.sml | 44 val parse = fn {arg : 'a, 83 saction(i,leftPos,stack,arg)
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | Assem.sml | 265 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list args); 267 List.map (fn arg => print (one_exp arg ^ " ")) (Binaryset.listItems rs); 269 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list outs);
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | Assem.sml | 265 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list args); 267 List.map (fn arg => print (one_exp arg ^ " ")) (Binaryset.listItems rs); 269 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list outs);
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | Assem.sml | 265 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list args); 267 List.map (fn arg => print (one_exp arg ^ " ")) (Binaryset.listItems rs); 269 List.map (fn arg => print (one_exp arg ^ " ")) (pair2list outs);
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | congLib.sml | 53 fun gen_refl(x as {Rinst,arg}) = mk_preorder_refl preorders Rinst x 64 val reflThm = refl {Rinst=preorderTerm,arg=var} 77 val reflThm = refl {Rinst=preorderTerm,arg=var} 83 (CONGPROC (fn {Rinst,arg} => REFL arg)) thm 288 fun conv thms tm = qconv thms tm handle _ => refl {Rinst=relation,arg=tm}
|
/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 178 val (v, body) = pairSyntax.dest_pabs arg 189 val arg = strip_comb_1 COND_PROP___EXISTS_term tt; value 190 val (v,b) = dest_abs arg 243 val arg = strip_comb_1 asl_exists_term tt; value 244 val (v,b) = dest_abs arg
|
/seL4-l4v-master/isabelle/src/Pure/Admin/ |
H A D | build_status.scala | 602 "D:" -> (arg => target_dir = Path.explode(arg)), 604 "S:" -> (arg => only_sessions = space_explode(',', arg).toSet), 605 "l:" -> (arg => options = options + ("build_log_history=" + arg)), 606 "o:" -> (arg => options = options + arg), 607 "s:" -> (arg => 608 space_explode('x', arg) [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | build_status.scala | 602 "D:" -> (arg => target_dir = Path.explode(arg)), 604 "S:" -> (arg => only_sessions = space_explode(',', arg).toSet), 605 "l:" -> (arg => options = options + ("build_log_history=" + arg)), 606 "o:" -> (arg => options = options + arg), 607 "s:" -> (arg => 608 space_explode('x', arg) [all...] |
/seL4-l4v-master/HOL4/src/datatype/mutrec/ |
H A D | Recftn.sml | 35 constructed with that constructor. If there is a variable "arg" with 230 let fun apply_all ftn (arg::args) = 231 apply_all (mk_comb {Rator = ftn, Rand = arg}) args 254 variable "arg" in order to allow the uxser to do something 259 let val arg_var = mk_var {Name = "arg", Ty = ftn_dom} 376 type atpat (since it's the second arg to constructor CONpat), and 404 fun get_rec_vars (all_vars, arg::more_args, rev_rec_vars) = 405 let val ftn_info = lookup_ftn (type_of arg, ftn_type_data) 409 (* can't recurse on this arg, so add no more vars *) 431 fun sort_cons_args (arg [all...] |
/seL4-l4v-master/HOL4/examples/hardware/hol88/tamarack2/ |
H A D | tamarack.ml | 116 (mem,mar,pc,acc,ir,arg,buf)) = 127 REG ((warg,gnd,bus,bus,arg),P) /\ 128 ALU (n+3) (alu0,alu1,arg,bus,alu) /\ 227 "Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) = 237 (mem,mar,pc,acc,ir,arg,buf))");;
|
/seL4-l4v-master/HOL4/examples/hardware/port/tamarack2/ |
H A D | tamarackScript.sml | 112 (mem,mar,pc,acc,ir,arg,buf)) = 123 REG ((warg,gnd,bus,bus,arg),P) /\ 124 ALU (n+3) (alu0,alu1,arg,bus,alu) /\ 223 ``Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) = 233 (mem,mar,pc,acc,ir,arg,buf))``);
|
/seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLib.sml | 241 ((not (all (fn arg => (type_of arg = word_type)) args)))) 273 fun translate_args arg = 274 if (numLib.is_numeral arg) then 275 ([], [term_to_string arg]) 279 get_word_fun_arity (type_of arg); 282 ("Invalid argument '" ^ (term_to_string arg) ^"' in term '"^(term_to_string exp)^"'!"); 284 translate_exp arg res_n 486 val args_string_list = map (fn arg => 487 word_type_string^ " "^(#1 (dest_var arg))) args_lis [all...] |
/seL4-l4v-master/HOL4/examples/HolCheck/examples/ |
H A D | amba_apb.sml | 42 fun apb_PSEL_proj i = if i<4 then apb_AP ("psel_"^(int_to_string i)) else failwith ("apb_PSEL_proj arg out of range") 52 fun apb_SADDR x = if x<2 then (apb_AP ("saddr_"^(int_to_string x))) else failwith ("apb_SADDR arg out of range") 53 fun apb_SDATA x = if x<2 then (apb_AP ("sdata_"^(int_to_string x))) else failwith ("apb_SDATA arg out of range")
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | timing.cpp | 124 POLYEXTERNALSYMBOL POLYUNSIGNED PolyTimingLocalOffset(FirstArgument threadId, PolyWord arg); 125 POLYEXTERNALSYMBOL POLYUNSIGNED PolyTimingSummerApplies(FirstArgument threadId, PolyWord arg); 126 POLYEXTERNALSYMBOL POLYUNSIGNED PolyTimingConvertDateStuct(FirstArgument threadId, PolyWord arg); 283 POLYUNSIGNED PolyTimingLocalOffset(FirstArgument threadId, PolyWord arg) argument 289 Handle pushedArg = taskData->saveVec.push(arg); 354 POLYUNSIGNED PolyTimingSummerApplies(FirstArgument threadId, PolyWord arg) argument 360 Handle pushedArg = taskData->saveVec.push(arg); 399 POLYUNSIGNED PolyTimingConvertDateStuct(FirstArgument threadId, PolyWord arg) argument 405 Handle pushedArg = taskData->saveVec.push(arg);
|
/seL4-l4v-master/HOL4/tools/mlyacc/mlyacclib/ |
H A D | MLY_parser1.sml | 66 val parse = fn {arg : 'a, 105 saction(i,leftPos,stack,arg)
|
/seL4-l4v-master/HOL4/polyml/ |
H A D | install-sh | 180 for arg 183 # $@ is not empty: it contains at least $arg. 187 shift # arg 188 dst_arg=$arg
|