/seL4-l4v-10.1.1/isabelle/Admin/Mercurial/ |
H A D | hgwebdir.cgi | 52 application = hgwebdir('/home/isabelle-repository/repos/hgweb.config') variable 53 wsgicgi.launch(application)
|
/seL4-l4v-10.1.1/l4v/isabelle/Admin/Mercurial/ |
H A D | hgwebdir.cgi | 52 application = hgwebdir('/home/isabelle-repository/repos/hgweb.config') variable 53 wsgicgi.launch(application)
|
/seL4-l4v-10.1.1/HOL4/src/enumfset/ |
H A D | inttoTacs.sml | 27 (* An integer ground term is, as well as I can see, either a application of 28 ``$&`` to a num ground term (which is either ``0`` or an application 29 of NUMERAL to a pile of ZERO, BIT0, and BIT1) or an application of 30 numeric_negate:int -> int to such a &-application. ``-0`` is considered
|
H A D | inttoScript.sml | 41 (* An integer ground term is, as well as I can see, either a application of 42 ``$&`` to a num ground term (which is either ``0`` or an application 43 of NUMERAL to a pile of ZERO, BIT0, and BIT1) or an application of 44 numeric_negate:int -> int to such a &-application. ``-0`` is possible. *)
|
/seL4-l4v-10.1.1/HOL4/src/num/theories/ |
H A D | numSyntax.sml | 91 (* Partial application of measure is often more useful *) 127 else raise ERR "dest_num_case" "not an application of \"num_CASE\"" 128 | _ => raise ERR "dest_num_case" "not an application of \"num_CASE\"" 135 else raise ERR "dest_funpow" "not an application of \"FUNPOW\"" 136 | _ => raise ERR "dest_funpow" "not an application of \"FUNPOW\""; 144 else raise ERR "dest_while" "not an application of \"WHILE\"" 145 | _ => raise ERR "dest_while" "not an application of \"WHILE\""; 152 else raise ERR "dest_divmod" "not an application of \"divmod\"" 153 | _ => raise ERR "dest_divmod" "not an application of \"divmod\""; 160 else raise ERR "dest_measure" "not an application o [all...] |
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | make_imported_acl2_theory.ml | 30 (* not using map to guarantee hd-to-tl application order *)
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | Arith_cons.sml | 126 (* Functions to extract the arguments from an application of a binary op. *) 133 (* Is a term a full application of a numerical relation? *)
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | translateLib.sml | 134 else raise_error "dest_acl2_cond" "not an application of \"ite\"" 135 | _ => raise_error "dest_acl2_cond" "not an application of \"ite\"" 151 of (acl2_cons,[a,b]) => if same_const acl2_cons acl2_cons_tm then (a,b) else raise_error "dest_acl2_cons" "not an application of \"cons\"" 152 | _ => raise_error "dest_acl2_cons" "not an application of \"cons\""; 166 of (acl2_true,[a]) => if same_const acl2_true acl2_true_tm then a else raise_error "dest_acl2_true" "Not an application of \"|=\"" 167 | _ => raise_error "dest_acl2_true" "Not an application of \"|=\"";
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | funcCall.sml | 34 (* Is an expression a function application? *) 150 if is_fun x andalso not (x = !tr_f) then (* non-recursive function application *) 160 mk_plet(v, caller_save M, caller_save N) (* not function application *) 192 if is_fun x andalso not (x = !tr_f) then (* non-recursive function application *) 206 in (mk_plet(v, M', N'), output') end (* not function application *)
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | ObsCongrConv.sml | 171 (* Conversion for the application of the tau-law TAU1: 191 (* Conversion for the application of the tau-law TAU2: 209 (* Conversion for the application of the tau-law TAU3: 251 (* Define the conversions for the application of the laws for OBS_CONGR 264 (* Define the tactics for the application of the laws for OBS_CONGR *)
|
H A D | StrongLawsConv.sml | 42 (* Conversion for the application of STRONG_SUM_IDENT(_L/R). *) 103 (* Conversion for the application of STRONG_SUM_IDEMP. *) 121 (* Conversion for the application of the laws for the restriction operator. *) 170 (* Conversion for the application of the laws for the relabelling operator. *) 304 (* Conversion for the application of the law for the parallel operator in the 356 (* Conversion for the application of the laws for the parallel operator in the 380 (* Conversion for the application of the laws for the parallel operator. *) 438 (* Tactics for the application of the laws for STRONG_EQUIV on the left-hand
|
H A D | ObsCongrLib.sml | 57 (* Convert a conversion for the application of the laws for OBS_CONGR to a
|
H A D | WeakEQLib.sml | 55 (* Convert a conversion for the application of the laws for STRONG_EQUIV to a
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/lambek/ |
H A D | LambekScript.sml | 998 val application = store_thm ("application", value 1005 val application' = store_thm ("application'", 1071 >> REWRITE_TAC [application]); 1082 >> REWRITE_TAC [application']); 1092 >> REWRITE_TAC [application']); 1102 >> REWRITE_TAC [application]); 1124 REWRITE_TAC [application] ]); 1144 REWRITE_TAC [application'] ]); [all...] |
/seL4-l4v-10.1.1/HOL4/examples/dev/dff/ |
H A D | dffScript.sml | 81 (* Put tempabs' in the correct form for application to D-type *)
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | intro.tex | 17 application domains. As a microkernel, it provides a small number of
|
H A D | objects.tex | 18 application domains. 26 application. Applications are limited to accessing memory in their 52 operation, an application must \emph{invoke} a capability in its 64 Conceptually, a capability resides in an application's \emph{capability 66 may not contain a capability. An application may refer to 81 access rights, the delegation of authority to another application, and 82 passing to an application authority to a newly created (or selected) 132 capability and the application to continue. If the invoked 234 scheduled, blocked, unblocked, etc., depending on the application's 292 Instead, objects must be explicitly created from application [all...] |
/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | syntax.tex | 78 application, or a lambda term. 98 & | & \term\ \term & \mbox{(application)} \\ 121 application can be iterated. Application is left associative so that
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | syntax.tex | 78 application, or a lambda term. 98 & | & \term\ \term & \mbox{(application)} \\ 121 application can be iterated. Application is left associative so that
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | PRINT_PARSETREE.sml | 162 (* Infixed application. *) 173 | Applic {f, arg, ...} => (* Function application. *) 263 (* Single infixed application. *) 276 (* Infixed application followed by other arguments. *) 291 (* Prefixed application. *)
|
/seL4-l4v-10.1.1/HOL4/src/compute/src/ |
H A D | computeLib.sml | 47 * this means we found a beta redex. mka rebuilds the application of 76 * - if we are done with the Rand of a const, we rebuild the application 78 * - an application to a NEUTR can be rebuilt only if the argument has been
|
/seL4-l4v-10.1.1/HOL4/src/datatype/ |
H A D | DatatypeSimps.sig | 60 lifting case constants. Use carefully, since their application
|
/seL4-l4v-10.1.1/HOL4/src/lite/ |
H A D | liteLib.sig | 26 * Some extra combinators, e.g. reverse application. *
|
/seL4-l4v-10.1.1/HOL4/src/pfl/ |
H A D | pflLib.sml | 37 fun dest_args [] = raise ERR "dest_args" "not enough args in function application"
|
/seL4-l4v-10.1.1/HOL4/src/simp/src/ |
H A D | Opening.sig | 51 * to rewrite under application. See the rule for restricted
|