| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | annotatedIR.sml | 60 (itlist (curry (fn (stm,str) => "; " ^ formatInst stm ^ str)) (tl stmL) "") ^ "]"))
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | annotatedIR.sml | 60 (itlist (curry (fn (stm,str) => "; " ^ formatInst stm ^ str)) (tl stmL) "") ^ "]"))
|
| /seL4-l4v-10.1.1/HOL4/src/num/theories/ |
| H A D | numeralScript.sml | 205 fun ncases str n0 =
208 (SPEC (mk_var(str, (==`:num`==))) num_CASES)
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | Parse.sml | 753 String.concat ["#", Lib.quote(str c)])
764 String.concat ["#", Lib.quote(str c)])
|
| H A D | type_grammar.sml | 108 | PARAM n => Type.mk_vartype ("'"^str (chr (n + ord #"a")))
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | Holmake.sml | 879 fun str (n,ni) = function
882 List.app (print o str) (listNodes g);
|
| H A D | basis2002.sml | 799 else String.extract(s,0,SOME i) ^ str c ^
1024 else String.translate (fn c => if c = #"/" then slash else str c) s
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
| H A D | derive_specsLib.sml | 679 val str = "Section `"^sec_name^"` consists of "^cl^" instructions." value
680 val _ = write_line str
|
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/ |
| H A D | muddy.c | 16 #include <mosml/str.h>
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_invScript.sml | 39 string_data str = n2w (LENGTH str + 1) :: MAP ((n2w:num->word8) o ORD) str`;
43 (symbol_list (str::xs) = string_data str ++ symbol_list xs)`;
2184 ?str p. (LENGTH str = n) /\
2185 ((one_byte_list sa2 str * p) (fun2set (g,dg))) /\
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
| H A D | assemblerML.sml | 763 let val h = mnemonic a ((if #L y then "ldr" else "str") ^
795 let val h = mnemonic a ((if #L y then "ldr" else "str") ^
|
| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | arm_disassemblerLib.sml | 112 String.str c ^ Int.toString n
701 f (opt (is_T unpriv) "t" (if is_T b then "strb" else "str"))
|
| /seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
| H A D | DerivedBddRules.sml | 206 SOME(str,_) => str
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
| H A D | DEBUGGER_.sml | 327 fun loadStruct (str as Struct { name, signat, locations, ...}, (decs, {staticEnv, dynEnv, lastLoc, ...})) =
329 val loadStruct = codeStruct (str, level)
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/ |
| H A D | vsynth.sml | 131 let val (str, [_,ty]) = dest_type(type_of tm) value
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
| H A D | Useful.sml | 692 val pp_char = pp_map str pp_string;
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | core_decompilerLib.sml | 65 val ESC = String.str (Char.chr 0x1B)
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/Examples/ |
| H A D | mlEdit.sml | 193 String.translate(fn #"\n" => "\r\n" | c => String.str c) s
|
| /seL4-l4v-10.1.1/HOL4/src/TeX/ |
| H A D | EmitTeX.sml | 37 | _ => String.str c)
|
| /seL4-l4v-10.1.1/HOL4/src/datatype/record/ |
| H A D | RecordType.sml | 125 mk_vartype("'" ^ String.str (Char.chr(Char.ord (String.sub(nm,0)) + 1)))
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibTerm.sml | 327 || some (fn c => c = #"~" orelse punct c) >> str) ++
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/mosml/ |
| H A D | Arbnumcore.sml | 463 str (if Int.<(n, 10)
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
| H A D | vars_as_resourceBaseFunctor.sml | 541 if c = #" " then Feedback.fail() else str c) v_st)
|
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | Useful.sml | 599 else str (Char.toUpper (String.sub (s,0))) ^ String.extract (s,1,NONE);
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | Useful.sml | 599 else str (Char.toUpper (String.sub (s,0))) ^ String.extract (s,1,NONE);
|