/seL4-l4v-master/HOL4/tools-poly/ |
H A D | smart-configure.sml | 54 fun loop cnt = function
|
/seL4-l4v-master/HOL4/src/opentheory/reader/ |
H A D | OpenTheoryReader.sml | 258 fun loop (x as {line_num,...}) = case TextIO.inputLine input of function
|
/seL4-l4v-master/HOL4/help/src-sml/ |
H A D | Doc2Tex.sml | 24 fun loop n = let function
|
H A D | ParseDoc.sml | 394 fun loop acc = function
|
H A D | Htmlsigs.sml | 275 let fun loop [] lineno = () function
|
/seL4-l4v-master/HOL4/src/AI/proof_search/ |
H A D | psMinimize.sml | 89 fun loop proof = case proof of function
|
/seL4-l4v-master/HOL4/src/holyhammer/ |
H A D | holyHammer.sml | 94 fun loop () = function
|
/seL4-l4v-master/HOL4/src/tactictoe/src/ |
H A D | tttBigSteps.sml | 182 fun loop acc anl_aux = function
|
/seL4-l4v-master/HOL4/examples/acl2/tests/inputs/ |
H A D | m1-story.lisp | [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | refine.sml | 50 let fun loop n acc = if n <= 0 then acc else loop(n-1) (#"0"::acc) function
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | Redblackset.sml | 118 let fun loop stack acc = function 129 let fun loop stack = get stack (fn x => (f x; loop)) () function 164 let fun loop ZERO power acc = acc function 187 let fun loop x y stack1 stack2 res = function 234 let fun loop x y stack1 stack2 = function 249 let fun loop x y stack1 stack2 = function 270 let fun loop x y stack1 stack2 res = function 295 let fun loop x y stack1 stack2 res = function 326 let fun loop k p = if p >= n then k else loop (k+1) (2*p) function [all...] |
H A D | OldPP.sml | 370 fun loop (instr) = function
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | SHA1_ML.sml | 170 fun loop (i, a, b, c, d, e) = function
|
H A D | MD5.sml | 43 fun loop [] = [] function 104 fun loop (i,digest) = function
|
/seL4-l4v-master/HOL4/tools/mlyacc/mlyacclib/ |
H A D | MLY_parser2.sml | 547 fun loop (lexPair,stack,queue,_,SOME ACCEPT) = function
|
/seL4-l4v-master/HOL4/tools/mlyacc/src/ |
H A D | lalr.sml | 474 fun loop true = () function
|
H A D | mklrtable.sml | 72 fun loop (h::t) = function 280 fun loop (nil,actions) = (rev actions,ERROR) function [all...] |
/seL4-l4v-master/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | parser2.sml | 529 fun loop (lexPair,stack,queue,_,SOME ACCEPT) = function
|
/seL4-l4v-master/l4v/isabelle/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/ |
H A D | parser2.sml | 529 fun loop (lexPair,stack,queue,_,SOME ACCEPT) = function
|
/seL4-l4v-master/HOL4/src/prekernel/ |
H A D | Lexis.sml | 120 let fun loop i = (Word8Array.sub(alphanumerics,ordof(str,i)) = bone) function 134 let fun loop i = (Word8Array.sub(tyvar_ids,ordof(str,i)) = bone) function 147 let fun loop i = (Word8Array.sub(hol_symbols,ordof(str,i)) = bone) function 211 let fun loop function [all...] |
/seL4-l4v-master/HOL4/tools/ |
H A D | configure.sml | 101 fun loop () = function 134 fun loop () = let function
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibArbnum.sml | 202 fun loop xn acc = function
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | Parse_support.sml | 414 fun loop ([v],E) = v E function
|
/seL4-l4v-master/HOL4/src/portableML/mosml/ |
H A D | Arbnumcore.sml | 240 fun loop xn acc = function
|
/seL4-l4v-master/HOL4/examples/PSL/regexp/ |
H A D | regexpTools.sml | 221 fun loop acc th = function
|