Searched refs:tag (Results 76 - 100 of 142) sorted by relevance

123456

/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/
H A DLEXSIG.sml65 ({ location: location, hard: bool, message: pretty, context: pretty option } -> unit) Universal.tag
H A DBUILTINS.sml50 | IsTaggedValue (* Test the tag bit. *)
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/
H A Dpresent.scala208 tags.map(tag =>
209 tag.toList match {
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/
H A Dpresent.scala208 tags.map(tag =>
209 tag.toList match {
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DLiteral.sml5 * inside the NUMERAL tag, or it is a straight ZERO constant. This
95 occasionally occur, for example when the NUMERAL tag has been rewritten
/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DThyDataSexp.sml183 case Tag.dep_of (Thm.tag th) of
192 tagwrite (Thm.tag th) ^
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/
H A Dprog_x64Lib.sml260 val tag = (RW [GSYM STAR_ASSOC] th) |> concl |> car value
262 val x1 = (cdr o cdr o car) tag
263 val x2 = (cdr o cdr) tag
264 val a = (cdr o car o cdr) tag
359 val tag = (RW [GSYM STAR_ASSOC] th) |> concl |> car
361 val x1 = (cdr o cdr o car) tag
362 val x2 = (cdr o cdr) tag
363 val a = (cdr o car o cdr) tag
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DBackendIntermediateCodeSig.sml84 | BICTagTest of { test: backendIC, tag: word, maxTag: word }
162 val tupleTag: Universal.universal list list Universal.tag
/seL4-l4v-10.1.1/l4v/camkes/glue-proofs/
H A DEventFrom.c698 tag member in struct:seL4_IPCBuffer_
H A DEventTo.c598 tag member in struct:seL4_IPCBuffer_
/seL4-l4v-10.1.1/seL4/manual/parts/
H A Dapi.tex84 \newcommand{\errorenumdesc}{A return value of \texttt{0} indicates success. A non-zero value indicates that an error occurred. See \autoref{sec:errors} for a description of the message register and tag contents upon error.}
113 seL4 system calls return an error code in the message tag and a short
/seL4-l4v-10.1.1/HOL4/polyml/libpolymain/
H A DMakefile.in141 libpolymain_la_LINK = $(LIBTOOL) $(AM_V_lt) --tag=CC \
163 LTCOMPILE = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \
172 LINK = $(LIBTOOL) $(AM_V_lt) --tag=CC $(AM_LIBTOOLFLAGS) \
/seL4-l4v-10.1.1/HOL4/src/floating-point/native/
H A Dselftest.sml48 case Tag.dest_tag (Thm.tag thm) of
/seL4-l4v-10.1.1/HOL4/src/marker/
H A DmarkerScript.sml84 For wrapping up abbreviations in the assumption list. This tag
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DTopLevelPolyML.sml570 (* Read the ASN1 header to get the tag and then read the data.
576 | SOME((tag, length), afterHdr) =>
585 (tag, vector)
590 SOME{tag, data, remainder} =>
591 (tag, data) :: splitSequence remainder
595 fun findData tag list =
596 Option.map #2 (List.find (fn (t, _) => t = tag) list)
598 fun findString tag list =
599 Option.map decodeString (findData tag list)
600 and findInt tag lis
[all...]
/seL4-l4v-10.1.1/HOL4/src/1/
H A DTypeBase.sml24 List [Sym tag, String str, Thm th] =>
25 if tag = simpfrag.simpfrag_conv_tag then
H A DSanity.sml91 val (oL, aL) = Tag.dest_tag (tag thm);
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DModel.sml269 fun mkEntry tag (na,n) = (tag,na,n);
271 fun mkList tag m = List.map (mkEntry tag) (NameArityMap.toList m);
273 fun ppEntry (tag,source_arity,target) =
275 [Print.ppString tag,
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DModel.sml269 fun mkEntry tag (na,n) = (tag,na,n);
271 fun mkList tag m = List.map (mkEntry tag) (NameArityMap.toList m);
273 fun ppEntry (tag,source_arity,target) =
275 [Print.ppString tag,
/seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/
H A DholfootParser.sml361 tag_a_expression_list2absyn vs rvm ((tag,exp1)::l) =
363 val tag_term = string2holfoot_tag tag;
809 | holfoot_p_statement2absyn funL resL gv vs (Pstm_fldlookup (v, expr, tag)) =
814 [Absyn.mk_AQ var_term, exp_a, Absyn.mk_AQ (string2holfoot_tag tag)]);
818 | holfoot_p_statement2absyn funL resL gv vs (Pstm_fldassign (expr1, tag, expr2)) =
823 exp1, Absyn.mk_AQ (string2holfoot_tag tag), exp2]);
H A DholfootScript.sml856 (FEVERY (\(tag,exp).
858 (THE (exp stack) = (heap ' loc) tag)) L)))`;
1310 Q.EXISTS_TAC `measure (\ (tag,startExp,(dtagL,t),endExpP). tree_size0 t)` THEN
7171 ((h1 = h2) /\ (!tag dl1 dl2. MEM (tag, dl1) data1 /\ MEM (tag, dl2) data2 ==> (dl1 = dl2)))``,
7213 !tag dl1 dl2. MEM (tag,dl1) data1 /\ MEM (tag,dl2) data2 ==> (HD dl1 = HD dl2)` by (
7234 `(LIST_TO_FMAP L1 ' tag s
[all...]
/seL4-l4v-10.1.1/HOL4/src/holyhammer/
H A DhhWriter.sml335 val d = (dep_of o tag) thm
360 let val f = depnumber_of o depid_of o dep_of o Thm.tag in
/seL4-l4v-10.1.1/HOL4/src/opentheory/postbool/
H A DOpentheory.sml88 val NUMERAL_conv = let (* wrap numeric literals in NUMERAL tag *)
109 strip the tag if Nonlit is raised *)
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/
H A Dsystem.tex1365 Per evitare la non validit�, � attaccato un \emph{tag} a ogni teorema che deriva
1366 da un oracolo. Questo tag � propagato attraverso ogni inferenza cui quel
1370 tag componenti del teorema. Un teorema dimostrato senza l'uso di
1371 oracoli avr� un tag vuoto, e pu� essere cos� considerato essere stato dimostrato
1383 che crea direttamente il teorema richiesto e attacca ad esso il tag
1384 dato. Il tag � creato attraverso una chiamata a
1389 Tag.read : string -> tag
1394 esterni, i tag sono usati per implementare alcune utili operazioni di `sistema'
1396 funzione \ml{mk\_thm}. Il tag \verb+MK_THM+ viene attaccato ad ogni
1399 derivate. Un altro tag � usat
[all...]
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttUnfold.sml340 | Code (a,tag) :: m =>
344 then split_codelevel_aux (i + 1) s (Code (a,tag) :: pl) m
346 then split_codelevel_aux (i - 1) s (Code (a,tag) :: pl) m
347 else split_codelevel_aux i s (Code (a,tag) :: pl) m

Completed in 169 milliseconds

123456