Searched refs:tag (Results 101 - 125 of 142) sorted by relevance

123456

/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A Dholfoot_pp_print.sml675 (fn (tag,exp) =>
676 (sys (Top, Top, Top) (d - 1) tag >>
696 (fn (tag,exp) =>
697 (sys (Top, Top, Top) (d - 1) tag >>
H A DholfootLib.sml1112 val (dataL2_h, dataL2) = trypluck (fn dt => let val (tag, dl) = pairSyntax.dest_pair dt in value
1113 if (aconv tag tag_t) then dt else Feedback.fail() end) dataL;
1138 (*resort points to to front and insert tag if necessary*)
1597 (* adds the given tag to the points to *)
1614 (* add tag *)
2370 val (tag, v) = pairSyntax.dest_pair ttt; value
2374 pairSyntax.mk_pair (tag, vl)
/seL4-l4v-10.1.1/HOL4/polyml/
H A DMakefile.in133 poly_LINK = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \
139 polyimport_LINK = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \
188 LTCOMPILE = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \
197 LINK = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \
H A Dltmain.sh2034 --tag=TAG use configuration variables from tag TAG
2177 # enable the TAGNAME tag. We also add TAGNAME to the global $taglist
2191 func_fatal_error "invalid tag name: $tagname"
2195 # Don't test for the "default" C tag, as we know it's
2210 func_error "ignoring unknown tag $tagname"
2377 --tag) test $# = 0 && func_missing_arg $_G_opt && break
2647 # if one wasn't chosen via the "--tag" command line option.
2694 # was found and let the user know that the "--tag" command
2698 func_fatal_error "specify a tag wit
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DThread.sml100 val getLocal: 'a Universal.tag -> 'a option
101 val setLocal: 'a Universal.tag * 'a -> unit
274 fun getLocal (t: 'a Universal.tag) : 'a option =
288 fun setLocal (t: 'a Universal.tag, newVal: 'a) : unit =
/seL4-l4v-10.1.1/graph-refine/
H A Dsyntax.py1174 def parse_and_install_all (lines, tag, skip_functions=None):
1184 if tag != None:
1185 target_objects.functions_by_tag[tag] = set (functions)
H A Dlogic.py1221 tag = p.node_tags[n][0]
1239 if site == '%s_IN' % tag]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A Ddefunctionalize.sml10 (* tag followed by a top-level call. *)
18 (* this function's free variables. The dispatch function examines the closure tag and *)
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/step/
H A Dcheri_stepScript.sml533 ``^st.c_capr 0w = capr0``, ``capr0.tag``, ``~capr0.sealed``,
534 ``^st.c_pcc.tag``, ``~^st.c_pcc.sealed``,
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttTools.sml698 (Dep.depnumber_of o Dep.depid_of o Tag.dep_of o Thm.tag) thm
702 (Dep.depidl_of o Tag.dep_of o Thm.tag) thm
H A DtttRecord.sml208 (Dep.depid_of o Tag.dep_of o Thm.tag) thm
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/
H A Dgraph_specsLib.sml257 val tag = first (can dest_call_tag) hs value
258 val fname = fst (dest_call_tag tag)
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/
H A Dxwindows.cpp5825 unsigned tag; member in struct:__anon117
5942 switch(T->tag)
5966 default: Crash ("Bad arg type %x",T->tag);
5980 /* (string,(v,tag)) */
5985 T->tag = UNTAGGED(SND(snd));
5991 switch(T->tag)
6017 default: Crash ("Bad arg type %x",T->tag);
6033 switch(T->tag)
6056 default: Crash ("Bad arg type %x",T->tag);
6345 /* (string,(v,tag))
[all...]
/seL4-l4v-10.1.1/l4v/camkes/glue-proofs/
H A DRPCFrom.c699 tag member in struct:seL4_IPCBuffer_
H A DRPCTo.c698 tag member in struct:seL4_IPCBuffer_
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DfolMapping.sml136 val tag = mk_prefix FOL_PREFIX; value
140 val fake_new_tyvar = mk_vartype o mk_prime o tag;
143 val fake_new_var = mk_var o (tag ## I);
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A DHolSat.tex81 Setting \t{show\_tags} to \t{true} makes the \HOL{} top-level print theorem tags. The \t{DISK\_THM} oracle tag has nothing to do with \t{HolSatLib}. It just indicates the use of theorems from \HOL{} libraries read in from permanent storage.
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/
H A DSIGNATURES.sml44 type 'a tag = 'a Universal.tag
46 val univEnter: univTable * 'a tag * string * 'a -> unit;
47 val univLookup: univTable * 'a tag * string -> 'a option;
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DsimpLib.sml51 fun mk_rewr_convdata (thm,tag) = let
58 conv = appconv (COND_REWR_CONV th, tag)} before
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DPrimitiveBddRules.sml112 datatype term_bdd = TermBdd of tag * assums * varmap * term * bdd.bdd;
231 then TermBdd(Tag.merge tg (Thm.tag th),HOLset.addList(ass,asl),vm,r,b)
/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dthreads.tex173 tag.
187 tag.
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_SIMPLIFIER.sml299 | simpGeneral context (TagTest{test, tag, maxTag}) =
303 if isShort testResult andalso toShort testResult = tag
306 | sTest => SOME(TagTest{test=sTest, tag=tag, maxTag=maxTag})
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DTheory.sml545 uptodate_axioms (Tag.axioms_of (Thm.tag thm))
595 val tags = Lib.set_diff (fst (Tag.dest_tag (Thm.tag th))) ["DISK_THM"]
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/
H A Dho_proverTools.sml1161 fun tag (f as (sub, FACT (CLAUSE (vars, _), _))) = ((vars, pinst sub tm), f) function
1162 val res = map snd (trans cons_subsume [] (map tag l))
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/
H A Dltmain.sh2034 --tag=TAG use configuration variables from tag TAG
2177 # enable the TAGNAME tag. We also add TAGNAME to the global $taglist
2191 func_fatal_error "invalid tag name: $tagname"
2195 # Don't test for the "default" C tag, as we know it's
2210 func_error "ignoring unknown tag $tagname"
2377 --tag) test $# = 0 && func_missing_arg $_G_opt && break
2647 # if one wasn't chosen via the "--tag" command line option.
2694 # was found and let the user know that the "--tag" command
2698 func_fatal_error "specify a tag wit
[all...]

Completed in 215 milliseconds

123456