| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | Z3_ProofParser.sml | 48 we re-use the SMT-LIB parser. *)
|
| /seL4-l4v-10.1.1/HOL4/src/emit/ |
| H A D | extended_emitScript.sml | 11 (* to re-create the functional aspect, via BAG_VAL. *)
|
| /seL4-l4v-10.1.1/HOL4/src/string/ |
| H A D | stringScript.sml | 287 (* Destruct a string. This will be used to re-phrase the HOL development *)
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | regexpMatch.sml | 276 then (print "re-encountering state.\n";
|
| H A D | Holmake_tools.sml | 732 built, and won't exist; mainly because the file we're trying to
|
| /seL4-l4v-10.1.1/graph-refine/ |
| H A D | rep_graph.py | 1240 import re namespace
1241 paren_w_re = re.compile (r"(\(|\)|\w+)")
|
| H A D | solver.py | 186 import re namespace
1979 paren_re = re.compile (r"(\(|\))")
2136 # this is awful, but happens sometimes because we're
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/extra/Win/ |
| H A D | Bitmap.sml | 393 (* GetBitmapBits and SetBitmapBits are supposedly obsolete but they're useful
|
| H A D | Window.sml | 539 (* Because we're using opaque matching we have to install pretty printers
|
| /seL4-l4v-10.1.1/HOL4/examples/fun-op-sem/for/ |
| H A D | for_compileScript.sml | 931 (* Start re-verification of phase1 in relational big step semantics *)
979 (* We now re-verify phase1 in the relational Pretty Big Step semantics (for terminating programs) *)
|
| /seL4-l4v-10.1.1/HOL4/src/IndDef/ |
| H A D | InductiveDefinition.sml | 22 Variants. We re-define the kernel "variant" function here because
799 (* here, generalise on the extra free variables if we're not being strict *)
|
| /seL4-l4v-10.1.1/HOL4/src/basicProof/ |
| H A D | BasicProvers.sml | 468 (* Add the rewrites into a simpset to avoid re-processing them when
535 (* Repeatedly do a case analysis anywhere in the goal. Avoids re-computing *)
|
| /seL4-l4v-10.1.1/HOL4/src/integer/ |
| H A D | CooperMath.sml | 596 is the variable we're going to eliminate, unless x can be entirely
768 (* phase three takes all of the coefficients of the variable we're
|
| H A D | OmegaSymbolic.sml | 630 eliminate divisibility terms, because we're not necessarily going
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | holfoot_pp_print.sml | 1271 val (f', wr, re, b) = dest_var_res_prop (COND_PROP___STRONG_EXISTS_term_rewrite p);
1274 val (rL, _) = bagSyntax.dest_bag re
|
| /seL4-l4v-10.1.1/HOL4/polyml/basis/ |
| H A D | BasicStreamIO.sml | 183 (* This stream was produced from re-reading a stream that already
644 then (* If the vector is too large to put in the buffer we're
|
| H A D | BoolArray.sml | 56 The equality function we're using tests all the bytes so we need to initialise them. *)
|
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | cacheTools.sml | 83 val re = List.nth(ll2,0) value
93 (*val _ = dbgTools.DTH (dpfx^ (ISPECL [le,re,q,p,x] envth))
95 val th = MP (ISPECL [le,re,q,p,x] envth) seqthm
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
| H A D | TYPEIDCODE.sml | 173 If we're only using type values for equality type variables the default
758 (* If this is a reference to a datatype we're currently generating
1070 (* If this is a type function we're going to generate a new ref anyway so we
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | Overload.sml | 261 they're equal, given that two types are equal if they can match
|
| /seL4-l4v-10.1.1/HOL4/src/real/ |
| H A D | realSimps.sml | 84 rewrites only apply when the variables look as if they're literals.
|
| /seL4-l4v-10.1.1/HOL4/tools/ |
| H A D | configure.sml | 530 (* Remove Poly/HOL executables from bin, if they're there *)
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | CODETREE_FUNCTIONS.sml | 348 (* This can arise if we're processing a branch of a case discriminating on
|
| H A D | CODETREE_LAMBDA_LIFT.sml | 98 (* Process the lambdas. Because they're mutually recursive this may set the
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
| H A D | TYPECHECK_PARSETREE.sml | 313 then (* It's not the last value and we're going to discard it *)
959 (* Add the structure we're opening here to the types of
1811 (* Unify this with the type we're using for the other clauses. *)
1832 local list to the recursive list. In that way if we're looking for whether a
|