Searched refs:final (Results 151 - 173 of 173) sorted by relevance

1234567

/seL4-l4v-master/HOL4/examples/CCS/
H A DMultivariateScript.sml2904 (* cleanups and renames before the final battle *)
2920 (* more cleanups before the final magic *)
2931 (* the final magic *)
/seL4-l4v-master/HOL4/src/quotient/examples/sigma/
H A DliftScript.sml1276 (* Melham and Gordon's fifth and final axiom. *)
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DcacheTools.sml319 (*val _ = dbgTools.DTH (dpfx^ th) val _ = dbgTools.DST (dpfx^ " final th\n") (*DBG*)*)
H A DcearTools.sml712 val cth = if (not (isSome ace)) (* final success theorem *)
H A DmuCheck.sml821 (* make final adjustments to result of model checking run
/seL4-l4v-master/isabelle/src/Doc/Logics/document/
H A DCTT.tex1244 The proof object has reached its final form. We call \ttindex{typechk_tac}
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics/document/
H A DCTT.tex1244 The proof object has reached its final form. We call \ttindex{typechk_tac}
/seL4-l4v-master/HOL4/examples/computability/turing/
H A Dturing_machine_primeqScript.sml1533 (* as final step, should show that we can extract number under head *)
/seL4-l4v-master/HOL4/src/parse/
H A Dterm_pp.sml860 One final wrinkle has to be dealt with:
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DTYPEIDCODE.sml1270 (* The final result function must take a single argument. *)
/seL4-l4v-master/HOL4/examples/acl2/examples/
H A DfmapExample.sml421 (* terminates in the final state s2. The evaluation relation is defined *)
627 (* where the postcondition is a relation between initial and final starts *)
/seL4-l4v-master/HOL4/src/probability/
H A DborelScript.sml4909 Induct_on `m` (* final induction *)
5081 (* Part VI: final strike *)
5708 (* final extreal arithmetics *)
5742 (* final real arithmetics *)
6870 (* final theorem (in this section): lborel and lebesgue coincide on borel *)
H A Dsigma_algebraScript.sml1973 (* final goal *)
H A DlebesgueScript.sml4488 (* final stage, applying pos_fn_integral_sub *)
/seL4-l4v-master/HOL4/src/quotient/examples/
H A Dind_rel.sml1420 (* final result is that
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/
H A DholfootLib.sml2985 (*build final theorem*)
/seL4-l4v-master/HOL4/polyml/basis/
H A DFinalPolyML.sml2 Title: Nearly final version of the PolyML structure
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DCODEGEN_PARSETREE.sml1508 (* Set the final addresses in case they have changed. N.B. Do this before
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dtactics.tex2070 that is saved of the interaction, aside from the final theorem.
/seL4-l4v-master/HOL4/examples/machine-code/lisp/
H A Dlisp_parseScript.sml3090 (* formulating the final theorem *)
/seL4-l4v-master/HOL4/examples/AKS/machine/
H A DcountPolyScript.sml3031 (* Note: the final poly_addM n p1 p2 can also be poly_addM n p2 p1, as addition is commutative.
/seL4-l4v-master/HOL4/src/coalgebras/
H A DllistScript.sml357 (* this is the uniqueness in the definition of llist as final coalgebra *)
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/
H A Dlisp_compiler_opScript.sml445 else if x0 = Val 1 then (* final case for let *)

Completed in 410 milliseconds

1234567