/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | CooperMath.sig | 73 function to have to re-call either term_of_int or int_of_term). *)
|
H A D | OmegaMLShadow.sml | 280 This records what sort of shadow we're currently working on. 284 (* REAL when we're looking for a contradiction (only) 285 DARK when we're looking for satisfiability and the problem is not 287 EXACT when we're looking for either a contradiction or satisfiability. 288 EDARK when we're looking for satisfiability (i.e., have switched from 411 (and they're all the same variable)
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | qbuf.sml | 15 field #4 : the frag list that we're consuming.
|
H A D | type_tokens.sml | 45 (* record whether or not we're onto part2 by checking if part2 is non-null *)
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | graph-refine.py | 24 import re namespace 119 word_re = re.compile('\\w+')
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | Timer.sml | 87 (* Override the default printer so they're abstract. *)
|
H A D | ExnPrinter.sml | 93 (* We keep a list in thread-local storage of refs we're currently printing.
|
H A D | Thread.sml | 160 signalled. When wait returns the mutex has been re-acquired. 166 The mutex is (re)acquired before Interrupt is delivered. *) 551 then (* We're done. *) 577 waitAgain() (* Wait and return the result when we're done. *) 583 (* Set this to handle interrupts synchronously unless we're already 644 (* Set this to handle interrupts synchronously unless we're already
|
H A D | FinalPolyML.sml | 589 | _ => (* No input waiting or we're at EOF. *) () 666 (* Exit if we've seen end-of-file or we're in the debugger 873 re-made to prevent them being made more than once, and it also prevents 956 (* Have we re-declared it ? *) 989 (* The name we're declaring may appear to be a dependency 1509 we're looking for matches the last component of the name 1545 (* This prints a block with the argument and, if we're exiting the result. 1584 name and we're not in the correct directory. *) 1701 debugging enabled while we're in the debugger we could 1759 raise Interrupt within the debuggee without re [all...] |
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/ |
H A D | imm_utils.py | 10 import re namespace
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Type.sml | 720 (* re ::= re "|" re *) 721 (* | re "&" re *) 722 (* | re <dot> re ;; <dot> is implicit because concat. is invisible *) 723 (* | ~re *) 724 (* | re<p> ;; p in {+,*,?} or a power or a range *) 725 (* | "(" re ")" *) [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_REMOVE_REDUNDANT.sml | 125 (* Check we're actually adding to the usage. *) 204 (* Get all the uses now we're finished and have identified 301 (* Remove unused arguments. They're unnecessary and may cause problems
|
/seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/cbv-lc/ |
H A D | typesScript.sml | 12 (* The call-by-value LC that we're building on *)
|
/seL4-l4v-10.1.1/HOL4/src/prekernel/ |
H A D | Globals.sml | 166 Flag telling us whether or not we're interactive.
|
/seL4-l4v-10.1.1/HOL4/src/compute/src/ |
H A D | computeLib.sml | 8 (* re-exporting types from clauses *) 264 (* sure that the constant doesn't get re-added when the theory is exported *)
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | internal_functions.sml | 204 val re = toRegexp c value 206 val m = regexpMatch.match re
|
H A D | Holdep.sml | 76 the .ui file too. We have to say that we're dependent
|
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/chronos/ |
H A D | emitter.py | 1 import re namespace
|
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
H A D | COPIER.sml | 70 the signature for values. This is needed because when we're constructing a signature 187 (* If we're copying it all set the resulting map to the new map. *)
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibOmega.sml | 318 This records what sort of shadow we're currently working on. 322 (* REAL when we're looking for a contradiction (only) 323 DARK when we're looking for satisfiability and the problem is not 325 EXACT when we're looking for either a contradiction or satisfiability. 326 EDARK when we're looking for satisfiability (i.e., have switched from 463 (and they're all the same variable)
|
/seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
H A D | quantHeuristicsLibBase.sml | 2917 fun HEURISTIC_QUANT_INSTANTIATE_CONV re min_occs heuristic expand_eq rwL ctx = 2918 (if re then REDEPTH_CONV else DEPTH_CONV) 2939 * - re : bool 2956 fun EXTENSIBLE_QUANT_INSTANTIATE_CONV cache_ref_opt re min_occs expand_eq ctx bqp args = 2958 HEURISTIC_QUANT_INSTANTIATE_CONV re min_occs (qp_to_heuristic arg cache_ref_opt) expand_eq (#final_rewrite_thms arg) ctx 2970 val (cache_ref_opt, re, filter, min_occs, expand_eq, args) = 2999 fun QUANT_INSTANTIATE_REDUCER cache_ref_opt re min_occs expand_eq bqp qpL = 3008 val res = EXTENSIBLE_QUANT_INSTANTIATE_CONV cache_ref_opt re min_occs expand_eq thms bqp qpL t; 3015 fun EXTENSIBLE_QUANT_INST_ss cache_ref_opt re min_occs expand_eq bqp qpL = 3016 simpLib.dproc_ss (QUANT_INSTANTIATE_REDUCER cache_ref_opt re min_occ [all...] |
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
H A D | WinBase.sml | 193 (* It seems that some other bits are set although they're not defined. *)
|
/seL4-l4v-10.1.1/HOL4/src/datatype/mutrec/ |
H A D | Recftn.sml | 251 if so, the constructor is the one we're looking for 324 function we're defining is the result type of the 385 types we're defining funtions on, and if so, whether the person is 542 and later we will get rid of the undesired fnI's that we're
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/mosml/ |
H A D | BuildCommand.sml | 118 (print ("Not re-running "^s^"Script; believe it will fail\n");
|
/seL4-l4v-10.1.1/HOL4/Manual/LaTeX/ |
H A D | ack.tex | 48 The material in the third edition constitutes a thorough re-working
|