/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | LEXSIG.sml | 65 ({ location: location, hard: bool, message: pretty, context: pretty option } -> unit) Universal.tag
|
H A D | BUILTINS.sml | 50 | IsTaggedValue (* Test the tag bit. *)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/ |
H A D | present.scala | 208 tags.map(tag => 209 tag.toList match {
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/ |
H A D | present.scala | 208 tags.map(tag => 209 tag.toList match {
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | Literal.sml | 5 * 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 D | ThyDataSexp.sml | 183 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 D | prog_x64Lib.sml | 260 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 D | BackendIntermediateCodeSig.sml | 84 | 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 D | EventFrom.c | 698 tag member in struct:seL4_IPCBuffer_
|
H A D | EventTo.c | 598 tag member in struct:seL4_IPCBuffer_
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | api.tex | 84 \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 D | Makefile.in | 141 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 D | selftest.sml | 48 case Tag.dest_tag (Thm.tag thm) of
|
/seL4-l4v-10.1.1/HOL4/src/marker/ |
H A D | markerScript.sml | 84 For wrapping up abbreviations in the assumption list. This tag
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | TopLevelPolyML.sml | 570 (* 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 D | TypeBase.sml | 24 List [Sym tag, String str, Thm th] => 25 if tag = simpfrag.simpfrag_conv_tag then
|
H A D | Sanity.sml | 91 val (oL, aL) = Tag.dest_tag (tag thm);
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Model.sml | 269 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 D | Model.sml | 269 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 D | holfootParser.sml | 361 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 D | holfootScript.sml | 856 (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 D | hhWriter.sml | 335 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 D | Opentheory.sml | 88 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 D | system.tex | 1365 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 D | tttUnfold.sml | 340 | 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
|