/seL4-l4v-master/HOL4/src/parse/ |
H A D | parse_term.sml | 322 val here = value 331 here @ rest 1301 (* need a rule here because
|
H A D | term_pp.sml | 288 here as the information generated here is not used to print 1287 (* if only rule is a list form rule and we've got to here, it
|
/seL4-l4v-master/HOL4/src/quotient/Manual/ |
H A D | quotient.tex | 951 %But the properties here describe a 1245 %which is here used as a prefix unary operator {\tt \$@}, 1924 We present here its proof in detail. 1967 The equality here is between functions, and by extension, true if 3000 which we will refer to from here on as $\xi$, 3253 The antecedent conjunct {\tt $R_i$ xi yi}, which here is {\tt xi = yi}, 4524 But an essential problem here is that the equality operation 4691 new type is used here, but sets are represented by the function type 4777 {\tt GSPEC} or {\tt IMAGE}. To make this clearer, here are the 5262 We here defin [all...] |
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | funCall.sml | 356 (* Note that callee's IP equals to caller's SP, we use the IP here to load the arguments *)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | funCall.sml | 344 (* Note that callee's IP equals to caller's SP, we use the IP here to load the arguments *)
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | CFLScript.sml | 285 (* No semantics is given here *)
|
H A D | funCall.sml | 341 (* Note that callee's IP equals to caller's SP, we use the IP here to load the arguments *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Menu.sml | 122 (* Check here means "make active", the opposite of uncheck *)
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | tcScript.sml | 497 Decided here not to call it "Floyd-Warshall algorithm", as Floyd's
|
/seL4-l4v-master/HOL4/src/portableML/mosml/ |
H A D | Arbnumcore.sml | 280 (* Knuth's algorithm is stateful so we mimic it here with
|
/seL4-l4v-master/HOL4/src/quotient/examples/ |
H A D | ind_rel.sml | 968 so it's now just MP. If there's a problem here, this may need to 996 {message = "this case should never happen, real problem here!", 1077 (* the goal here is to prove |- tm = T. I have |- rule so the goal is to 1539 term here looks like:
|
/seL4-l4v-master/HOL4/src/quotient/examples/sigma/ |
H A D | objectScript.sml | 593 (* Naive substitution; not proper; only here for pedagogical reasons. *)
|
/seL4-l4v-master/HOL4/src/res_quan/src/ |
H A D | res_quanLib.sml | 464 (* The auxiliary functions used here are taken from the system directly. *)
|
/seL4-l4v-master/HOL4/examples/Crypto/TWOFISH/ |
H A D | twofishScript.sml | 234 (* (here k = 4) of 32-bit words of and produces one word of output. This *)
|
/seL4-l4v-master/HOL4/examples/PSL/1.1/official-semantics/ |
H A D | LemmasScript.sml | 757 THEN IMP_RES_TAC (* Not sure why DECIDE_TAC fails here! *)
|
/seL4-l4v-master/HOL4/examples/PSL/path/ |
H A D | FinitePSLPathScript.sml | 165 * SEL_REC defined here is a fully specified version of SEG from
|
/seL4-l4v-master/HOL4/examples/acl2/examples/LTL/ |
H A D | LTLScript.sml | 141 * (Note: the transition relation is here not required to be total)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | BoolArray.sml | 23 (* We use int here for the length rather than word because the number of bits
|
/seL4-l4v-master/HOL4/examples/lambda/other-models/ |
H A D | raw_syntaxScript.sml | 14 The raw syntax here and the relations on it are taken from
|
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_opsemScript.sml | 321 (erase_eflags ii)) (* here erase_flag is an over approximation *)))) /\
|
/seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
H A D | test.ml | 413 (* NB: The regexp we have written here to recognize the contents of message *)
|
/seL4-l4v-master/HOL4/examples/miller/miller/ |
H A D | miller_rabinScript.sml | 806 >> EQ_TAC >| (* 2 sub-goals here *)
|
/seL4-l4v-master/HOL4/examples/miller/prob/ |
H A D | prob_uniformScript.sml | 507 >> REWRITE_TAC [real_lte] >| (* 3 sub-goals here *)
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | fcpScript.sml | 275 local (* and here the palaver to make this persistent; this should be easier
|
/seL4-l4v-master/HOL4/src/topology/ |
H A D | topologyScript.sml | 10 general topology theorems without using real numbers should be put here.
|