/seL4-l4v-10.1.1/graph-refine/ |
H A D | search.py | 465 if type (s) == str: 587 if type (p) != str] 1153 trace ('Testing guess for pair: %s' % str (pair)) 1219 if str (it[1][1]) == 'InductFailed'] 1693 return str (n) 1722 printout ("Decided to case split at %s" % str (details)) 1727 printout ('Found a future induction at %s' % str (details[0]))
|
H A D | stack_logic.py | 146 trace (str (vs)) 147 trace (str (hyps)) 224 trace (str ([hyp] + hyps))
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 205 iss.str(line);
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
H A D | extendTranslateScript.sml | 1393 val STRING_STRCAT = prove(``str (STRCAT s1 s2) = acl2_strcat (str s1) (str s2)``, 1408 val STRING_PREFIX = prove(``bool (isPREFIX s1 s2) = ite (not (less (length (str s2)) (length (str s1)))) 1409 (equal (coerce (str s1) (sym "COMMON-LISP" "LIST")) (acl2_take (length (str s1)) (coerce (str s2) (sym "COMMON-LISP" "LIST")))) nil``,
|
H A D | acl2encodeLib.sml | 218 {const = ``str``,definition = combinTheory.I_THM, induction = NONE}; 242 (simple_encode_map_encode ``str``) 254 ("str ?", op&&& o (equal ``str`` ## stringSyntax.is_string_literal) o dest_comb);
|
H A D | sexp.sml | 272 (* `(stringp(str x) = t) /\ (stringp _ = nil)`; *) 1202 ("(str " ^ "\"" ^ s ^ "\")") 1221 ("(str " ^ "\"" ^ s ^ "\")") 1242 ``str ^(abbrevMLstring s)`` 1264 | mlsexp_to_string (mlstr s) = ("(str " ^ "\"" ^ s ^ "\")") 1349 | mlsexp_to_term (mlstr s) = ``str ^(abbrevMLstring s)``
|
/seL4-l4v-10.1.1/l4v/misc/regression/ |
H A D | run_tests.py | 335 return ("Exception launching timeout_output: %s" % str(e))
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/decompiler/ |
H A D | arm_decomp_demoScript.sml | 155 e52d4004 (* push {r4} ; (str *)
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | parse_type.sml | 195 "'" ^ str (Char.chr (i - 0x3B1 + Char.ord #"a"))
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/ |
H A D | lisp_gcScript.sml | 53 E4835004 (* L2:str r5,[r3],#4 *) 54 E4836004 (* str r6,[r3],#4 *)`; 68 E4895004 (* str r5,[r9],#4 *) 80 E509501C (* str r5,[r9,#-28] *) 83 E5895004 (* str r5,[r9,#4] *) 104 E5893000 (* str r3,[r9] *)`; 113 E5093018 (* str r3,[r9,#-24] *) 114 E5094014 (* str r4,[r9,#-20] *) 115 E5095010 (* str r5,[r9,#-16] *) 116 E509600C (* str r [all...] |
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Print.sml | 49 val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape 59 | NONE => str c 117 fun charWord c = mkWord (str c);
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Print.sml | 49 val escapeMap = List.map (fn c => (c, "\\" ^ str c)) escape 59 | NONE => str c 117 fun charWord c = mkWord (str c);
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/correctness/ |
H A D | correctScript.sml | 392 ~(ic = mla_mul) /\ ~(ic = ldr) /\ ~(ic = str) /\ ~(ic = ldm) /\ 960 val _ = print "*\nVerifying: swp, ldr, str\n*\n"; (*=========================*) 965 (DECODE_INST ireg IN {swp; ldr; str}) /\ (aregn2 = 2w) /\ 1927 \\ Cases_on `DECODE_INST ireg IN {swp; ldr; str}` 2004 DECODE_INST ireg IN {swp; ldr; str} \/ 2066 DECODE_INST ireg IN {swp; ldr; str} \/
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/ |
H A D | sexp.sml | 297 (* `(stringp(str x) = t) /\ (stringp _ = nil)`; *) 1276 ("(str " ^ "\"" ^ s ^ "\")") 1295 ("(str " ^ "\"" ^ s ^ "\")") 1316 ``str ^(abbrevMLstring s)`` 1338 | mlsexp_to_string (mlstr s) = ("(str " ^ "\"" ^ s ^ "\")") 1423 | mlsexp_to_term (mlstr s) = ``str ^(abbrevMLstring s)``
|
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/ |
H A D | sexp.sml | 272 (* `(stringp(str x) = t) /\ (stringp _ = nil)`; *) 1202 ("(str " ^ "\"" ^ s ^ "\")") 1221 ("(str " ^ "\"" ^ s ^ "\")") 1242 ``str ^(abbrevMLstring s)`` 1264 | mlsexp_to_string (mlstr s) = ("(str " ^ "\"" ^ s ^ "\")") 1349 | mlsexp_to_term (mlstr s) = ``str ^(abbrevMLstring s)``
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
H A D | TYPECHECK_PARSETREE.sml | 900 SOME str => SOME(str, location) 910 fun copyEntries (str as Struct{locations, signat = sigTbl, name=strName, ...}, varLoc) = 935 List.map (fn c => mkSelectedVar (c, str, openLocs)) valConstrs) 944 makeSelectedStruct (strVal, str, openLocs); 953 mkSelectedVar (value, str, openLocs);
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Prim_rec.sml | 412 fun pass str = 413 if (mem str (!slist)) 416 else (slist := str :: !slist; str)
|
/seL4-l4v-10.1.1/HOL4/src/emit/ |
H A D | extended_emitScript.sml | 365 \ (String.^(String.str (Char.chr 1), s))"
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibUseful.sml | 597 val pp_char = pp_map str pp_string;
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/poly/ |
H A D | ProcessMultiplexor.sml | 401 (fn (c, (cs, n)) => ((str (chr n), (c, Waiting))::cs, n + 1))
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_symbolsScript.sml | 415 null_term_str a df f str = 416 ?p. (one_string a (str ++ [CHR 0]) * p) (fun2set (f,df)) /\ 417 EVERY (\x. ~(x = CHR 0)) str`; 420 exists_null_term_str a df f = ?str. null_term_str a df f str`; 423 mem2string a df f = @str. null_term_str a df f str`; 3047 \\ `(str = []) \/ ?x l. str = SNOC x l` by METIS_TAC [rich_listTheory.SNOC_CASES]
|
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/parse/ |
H A D | lisp_parseScript.sml | 1257 \\ `?str ps. sexp2abbrevt_aux exp T abbrevs {} = (str,ps)` by METIS_TAC [PAIR] 1271 string2sexp str = (sexp_parse (FST (sexp_lex str)))`;
|
/seL4-l4v-10.1.1/HOL4/Manual/Tools/ |
H A D | polyscripter.sml | 208 fun addIndent ws = String.translate(fn #"\n" => "\n"^ws | c => str c)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | lemmasScript.sml | 323 `!i. (DECODE_INST i = str) ==> ~(i %% 20)`,
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
H A D | annotatedIR.sml | 70 (itlist (curry (fn (stm,str) => "; " ^ formatInst stm ^ str)) (tl stmL) "") ^ "]"))
|