| /seL4-l4v-master/HOL4/src/parse/ |
| H A D | qbuf.sig | 13 val advance : 'a qbuf -> unit value
|
| H A D | qbuf.sml | 99 fun advance r = case !r of (lbopt, ((curr,cloc), rest), nf_q, q) => function
|
| H A D | ParseDatatype.sml | 127 fun advance () = qbuf.advance qb function
|
| H A D | term_tokens.sml | 424 val {advance,replace_current} = qb value
[all...] |
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibResolution.sig | 37 val advance : resolution -> resolution option (* select deduce factor add *) value
|
| H A D | mlibResolution.sml | 208 fun advance res = function
|
| H A D | mlibSolver.sml | 101 fun advance NONE s = (SOME NONE, s) function
|
| /seL4-l4v-master/HOL4/tools/Holmake/ |
| H A D | parse_glob.sml | 11 fun advance (s,i) = (s, i + 1) function
|
| H A D | Holdep_tokens.sml | 42 fun advance (c as CR {pos, buffer, maxpos, reader, current, closer}) = function
|
| H A D | ReadHMF.sml | 50 fun advance (b as B r) = function
[all...] |
| /seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
| H A D | ho_discrimTools.sml | 89 fun advance COMB_BEGIN state = state function
186 fun advance (FVAR (fv, fbs)) ((bvs, RIGHT tm::rest), (sub, thks)) = function
231 fun advance (FVAR (fv, fbs)) ((bvs, RIGHT tm :: rest), sub) = function
[all...] |
| H A D | skiTools.sml | 235 fun advance (SKI_VAR v) (RIGHT tm :: rest, sub) = (rest, raw_match' v tm sub) function
255 fun advance _ pat (SOME (v, lstate), rstate, work) = function
[all...] |
| H A D | ho_proverTools.sml | 466 fun advance lit (changed, lits', rules') = function
|
| /seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
| H A D | Dialog.sml | 230 fun advance () = function
|
| /seL4-l4v-master/HOL4/Manual/Tools/ |
| H A D | polyscripter.sml | 35 fun advance (LB {strm, currentOpt, line}) = function
[all...] |
| /seL4-l4v-master/HOL4/examples/formal-languages/context-free/ |
| H A D | grammarLib.sml | 109 fun advance c p = if c = #"\n" then newline p else add1col p function
|