Searched refs:application (Results 1 - 25 of 168) sorted by relevance

1234567

/seL4-l4v-10.1.1/isabelle/Admin/Mercurial/
H A Dhgwebdir.cgi52 application = hgwebdir('/home/isabelle-repository/repos/hgweb.config') variable
53 wsgicgi.launch(application)
/seL4-l4v-10.1.1/l4v/isabelle/Admin/Mercurial/
H A Dhgwebdir.cgi52 application = hgwebdir('/home/isabelle-repository/repos/hgweb.config') variable
53 wsgicgi.launch(application)
/seL4-l4v-10.1.1/HOL4/src/enumfset/
H A DinttoTacs.sml27 (* 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 DinttoScript.sml41 (* 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 DnumSyntax.sml91 (* 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 Dmake_imported_acl2_theory.ml30 (* not using map to guarantee hd-to-tl application order *)
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/
H A DArith_cons.sml126 (* 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 DtranslateLib.sml134 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 DfuncCall.sml34 (* 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 DObsCongrConv.sml171 (* 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 DStrongLawsConv.sml42 (* 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 DObsCongrLib.sml57 (* Convert a conversion for the application of the laws for OBS_CONGR to a
H A DWeakEQLib.sml55 (* 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 DLambekScript.sml998 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 DdffScript.sml81 (* Put tempabs' in the correct form for application to D-type *)
/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dintro.tex17 application domains. As a microkernel, it provides a small number of
H A Dobjects.tex18 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 Dsyntax.tex78 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 Dsyntax.tex78 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 DPRINT_PARSETREE.sml162 (* 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 DcomputeLib.sml47 * 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 DDatatypeSimps.sig60 lifting case constants. Use carefully, since their application
/seL4-l4v-10.1.1/HOL4/src/lite/
H A DliteLib.sig26 * Some extra combinators, e.g. reverse application. *
/seL4-l4v-10.1.1/HOL4/src/pfl/
H A DpflLib.sml37 fun dest_args [] = raise ERR "dest_args" "not enough args in function application"
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DOpening.sig51 * to rewrite under application. See the rule for restricted

Completed in 202 milliseconds

1234567