| /seL4-l4v-10.1.1/HOL4/polyml/modules/IntInfAsInt/ |
| H A D | StringChar.sml | 37 val extract = fn(s, i, j) => extract(s, FixedInt.fromInt i, Option.map FixedInt.fromInt j) value
47 val extract = fn(s, i, j) => extract(s, FixedInt.fromInt i, Option.map FixedInt.fromInt j) value
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | Literal.sml | 172 fun extract(i,c) = String.extract(s,i,c) function
|
| /seL4-l4v-10.1.1/HOL4/tools/mlyacc/mlyacclib/ |
| H A D | MLY_base-sig.sml | 232 val extract : svalue -> result value
|
| /seL4-l4v-10.1.1/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
| H A D | base.sig | 208 val extract : svalue -> result value
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
| H A D | base.sig | 208 val extract : svalue -> result value
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | Holmake_types.sml | 61 val extract = extract_quotation0 cmd value
[all...] |
| H A D | basis2002.sml | 700 val extract : string * int * int option -> substring value
|
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | StringSignatures.sml | 75 val extract : (string * int * int option) -> string value
120 val extract : (string * int * int option) -> substring value
|
| H A D | String.sml | 326 fun extract (s, i, NONE) = substring (s, i, size s - i) function
1268 val extract : (string * int * int option) -> substring value
1370 fun extract(s, i, NONE) = substring(s, i, String.size s-i) function
|
| H A D | FinalPolyML.sml | 2193 fun extract (tag:'a Universal.tag): Universal.universal list -> 'a list = function
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibArbnum.sml | 7 fun extract arg = ArraySlice.vector(ArraySlice.slice arg) function
|
| H A D | mlibModel.sml | 264 fun extract N = function
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/mosml/ |
| H A D | Arbnumcore.sml | 11 fun extract arg = ArraySlice.vector(ArraySlice.slice arg) function
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/poly/ |
| H A D | MD5.sml | 14 fun extract (vec, s, l) = function
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | OmegaMLShadow.sml | 34 fun extract x = VectorSlice.vector(VectorSlice.slice x) function
|
| /seL4-l4v-10.1.1/HOL4/tools/mlyacc/src/ |
| H A D | yacc-grm.sml | 846 val extract = fn a => (fn MlyValue.BEGIN x => x value
|
| /seL4-l4v-10.1.1/l4v/tools/c-parser/tools/mlyacc/src/ |
| H A D | yacc-grm.sml | 849 val extract = fn a => (fn MlyValue.BEGIN x => x value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/ |
| H A D | helperLib.sml | 1145 fun extract tm = let function
1154 fun extract tm = let function
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfootParser.sml | 1204 fun extract (Pfundecl(assume_opt, funname, (ref_args, val_args), rwOpt, preCondOpt, localV, function
|
| /seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
| H A D | Defn.sml | 514 fun extract FV congs f (proto_def,WFR) = function
|