/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | ExnPrinter.sml | 45 fun stringException(s, arg: string) = 46 parameterException(s, PolyML.prettyRepresentation(arg, depth-1))
|
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | isabelle.scala | 433 (name, arg) <- Token.read_antiq_arg(Keyword.Keywords.empty, body_text) 440 if (arg.isEmpty) "" 441 else if (Isabelle_Encoding.is_active(buffer)) Symbol.cartouche_decoded(arg.get) 442 else Symbol.cartouche(arg.get)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | isabelle.scala | 433 (name, arg) <- Token.read_antiq_arg(Keyword.Keywords.empty, body_text) 440 if (arg.isEmpty) "" 441 else if (Isabelle_Encoding.is_active(buffer)) Symbol.cartouche_decoded(arg.get) 442 else Symbol.cartouche(arg.get)
|
/seL4-l4v-master/HOL4/src/compute/src/ |
H A D | computeLib.sml | 57 * Precondition: f(arg) is a closure corresponding to b. 58 * Given (arg,(|- M = (a b), Stk)), 59 * returns (|- a = a, (<fun>,(|- b = b, f(arg)))::Stk) 62 fun push_in_stk f (arg,(th,stk)) = 64 (tha, Cbv_rator{Rand=(mka,(thb,f arg)), Ctx=stk}) 67 fun push_skip_stk f (arg,(th,stk)) = 69 (tha, Cbv_rand{Rator=(Lib.C mka,true,(thb,f arg)), Ctx=stk}) 98 - If the RHS is an abstraction and there is one arg on the stack, this means
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/computer/ |
H A D | proof2.ml | 146 i n assumptions (buf,m,mar,pc,acc,ir,arg,mpc,ready) = 148 then (buf,m,mar,pc,acc,ir,arg,mpc,ready) 152 ([buf;m;mar;pc;acc;ir;arg;mpc] @ assumptions) 172 let (buf,m,mar,pc,acc,ir,arg,mpc,readylist) =
|
/seL4-l4v-master/HOL4/src/TeX/ |
H A D | holindex.lex | 2 type arg = int;
|
/seL4-l4v-master/HOL4/src/compute/examples/ |
H A D | Arith.sml | 39 * strongly (arg of a free var), but we will have to reduce the
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | Arbrat.sml | 53 then raise Fail "inv: arg = 0"
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | internal_functions.sml | 247 fun which arg = 253 val fname = OS.Path.concat(p, arg) 270 fun shell arg = 286 val proc = execute ("/bin/sh", ["-c", arg])
|
H A D | Holmake_tools.sml | 657 fun runholdep {ofs, extras, includes, arg, destination} = let 660 val _ = chatty ("Analysing "^fromFile arg) 676 val _ = diagK ("Running Holdep on "^fromFile arg^" with includes = [" ^ 681 includes = includes, fname = fromFile arg} 774 val arg = holdep_arg f (* arg is file to analyse for dependencies *) value 777 if isSome arg then let 778 val arg = valOf arg value 779 val argname = fromFile arg [all...] |
/seL4-l4v-master/isabelle/src/Pure/Admin/ |
H A D | components.scala | 290 "o:" -> (arg => options = options + arg),
|
H A D | build_fonts.scala | 351 "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
|
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | simplifier_trace.scala | 172 consume = (arg: Any) => 174 arg match {
|
/seL4-l4v-master/HOL4/examples/temporal_deep/src/tools/ |
H A D | congToolsLib.sml | 39 val reflThm = refl {Rinst=preorderTerm,arg=var}
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
H A D | components.scala | 290 "o:" -> (arg => options = options + arg),
|
H A D | build_fonts.scala | 351 "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | simplifier_trace.scala | 172 consume = (arg: Any) => 174 arg match {
|
/seL4-l4v-master/HOL4/tools/Holmake/mosml/ |
H A D | BuildCommand.sml | 57 fun build_command g (ii as {preincludes,includes}) c arg = let 65 val file = fromFile arg 66 val intp = case arg of SML (Script _) => true | _ => false
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | testutils.sml | 251 fun shouldfail {printarg,testfn,printresult,checkexn} arg = 253 val _ = tprint (printarg arg) 257 require_msg check printresult testfn arg
|
H A D | Parse_support.sml | 435 fun itthis (bvs, arg) {body_bvars,args,E} = let 437 val (arg',E') = 438 case rst of [] => arg E | L => bind_term l L arg E 440 {body_bvars = b::body_bvars, args=arg'::args, E=E'} 445 fun rev_itthis arg (core, E) = 449 (Comb{Rator= Comb{Rator=let_t, Rand=core,Locn=l},Rand=arg,Locn=l},
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | basicio.cpp | 163 POLYEXTERNALSYMBOL POLYUNSIGNED PolyChDir(FirstArgument threadId, PolyWord arg); 164 POLYEXTERNALSYMBOL POLYUNSIGNED PolyBasicIOGeneral(FirstArgument threadId, PolyWord code, PolyWord strm, PolyWord arg); 615 POLYUNSIGNED PolyChDir(FirstArgument threadId, PolyWord arg) argument 621 Handle pushedArg = taskData->saveVec.push(arg); 1066 POLYUNSIGNED PolyBasicIOGeneral(FirstArgument threadId, PolyWord code, PolyWord strm, PolyWord arg) argument 1074 Handle pushedArg = taskData->saveVec.push(arg);
|
/seL4-l4v-master/HOL4/src/AI/sml_inspection/ |
H A D | smlParallel.sml | 234 fun widarg_file pd wid = wid_dir pd wid ^ "/arg" 371 val arg = (#read_arg es) (widarg_file pd wid) value 372 val r = (#function es) param arg 427 write_arg = let fun f file arg = writel file [its arg] in f end,
|
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | defunctionalize.sml | 178 List.map (fn arg => 180 Tyop = M.find(!ClosName, type_of arg) 181 handle e => #1 (Type.dest_type (type_of arg))}) 286 val arg = mk_pair(clos_arg, f_arg) value 287 val lt = mk_comb(df_var, arg) 334 val (arg, body) = dest_pabs M value 335 val _ = convert_fun (mk_eq(mk_comb(v, arg), body))
|
/seL4-l4v-master/HOL4/tools/mlyacc/mlyacclib/ |
H A D | MLY_parser2.sml | 222 fn (table,showTerminal,saction,fixError,arg) => 244 (case saction(i,leftPos,stack,arg) 271 fn (table,showTerminal,saction,arg) => 292 (case saction(i,leftPos,stack,arg) 535 val parse = fn {arg,table,lexer,saction,void,lookahead, 544 val distanceParse = distanceParse(table,showTerminal,saction,arg) 546 val ssParse = ssParse(table,showTerminal,saction,fixError,arg)
|
/seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | parser2.sml | 194 fn (table,showTerminal,saction,fixError,arg) => 216 (case saction(i,leftPos,stack,arg) 243 fn (table,showTerminal,saction,arg) => 264 (case saction(i,leftPos,stack,arg) 517 val parse = fn {arg,table,lexer,saction,void,lookahead, 526 val distanceParse = distanceParse(table,showTerminal,saction,arg) 528 val ssParse = ssParse(table,showTerminal,saction,fixError,arg)
|