/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfoot_pp_print.sml | 675 (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 D | holfootLib.sml | 1112 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 D | Makefile.in | 133 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 D | ltmain.sh | 2034 --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 D | Thread.sml | 100 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 D | syntax.py | 1174 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 D | logic.py | 1221 tag = p.node_tags[n][0] 1239 if site == '%s_IN' % tag]
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | defunctionalize.sml | 10 (* 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 D | cheri_stepScript.sml | 533 ``^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 D | tttTools.sml | 698 (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 D | tttRecord.sml | 208 (Dep.depid_of o Tag.dep_of o Thm.tag) thm
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | graph_specsLib.sml | 257 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 D | xwindows.cpp | 5825 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 D | RPCFrom.c | 699 tag member in struct:seL4_IPCBuffer_
|
H A D | RPCTo.c | 698 tag member in struct:seL4_IPCBuffer_
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | folMapping.sml | 136 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 D | HolSat.tex | 81 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 D | SIGNATURES.sml | 44 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 D | simpLib.sml | 51 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 D | PrimitiveBddRules.sml | 112 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 D | threads.tex | 173 tag. 187 tag.
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_SIMPLIFIER.sml | 299 | 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 D | Theory.sml | 545 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 D | ho_proverTools.sml | 1161 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 D | ltmain.sh | 2034 --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...] |