/seL4-l4v-master/HOL4/src/probability/ |
H A D | borelScript.sml | 457 (* `fn_plus f x + fn_minus f x` is always defined (same reason as above) *) 1773 (* the same theorems with more meaningful names, new *) 4025 fs [Borel, PREIMAGE_UNION, UNION_OVER_INTER'] (* 3 subgoals, same tactics *) \\ 4153 (* 2 subgoals, same tactics below *) 5413 (* "open" (J) and "half open" (H) intervals of the same bounds *) 5920 >- fs [REAL_LE_LT] \\ (* 2 goals left, same tactics *) 6942 >> EQ_TAC >> rpt STRIP_TAC >> Q.EXISTS_TAC `N` (* 2 subgoals, same tactics *) 8138 fs [Borel, PREIMAGE_UNION, UNION_OVER_INTER'] (* 3 subgoals, same tactics *) \\ 9098 fs [Borel, PREIMAGE_UNION, UNION_OVER_INTER'] (* 3 subgoals, same tactics *) \\
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | Conv.sml | 707 then raise ERR "AND_FORALL_CONV" "forall'ed variables not the same" 787 raise ERR "OR_EXISTS_CONV" "Variables not the same"
|
/seL4-l4v-master/HOL4/Manual/Translations/IT/Logic/ |
H A D | semantics.tex | 283 \PPL\index{PPlambda (same as PPLAMBDA), of LCF system@\ml{PP}$\lambda$ (same as \ml{PPLAMBDA}), of \ml{LCF} system}, dal momento che \HOL{} � stato
|
/seL4-l4v-master/HOL4/examples/simple_complexity/loop/ |
H A D | loopDecreaseScript.sml | 693 (* This is the same as hop_exceeds: |- !b n. 0 < b ==> n <= b * hop b n *) 1942 (* This is the same, but directly from the SUM *)
|
H A D | loopDivideScript.sml | 801 (* This is the same as pop_exceeds: |- !b n. 1 < b ==> n < b ** pop b n *) 2030 (* This is the same, but directly from the SUM *)
|
/seL4-l4v-master/HOL4/examples/fun-op-sem/ml/ |
H A D | typeSoundScript.sml | 86 apply them; in our syntax we can of course achieve the same in e by: 1605 value has the same type as the original expression, and if they terminate with
|
/seL4-l4v-master/HOL4/examples/algebra/ring/ |
H A D | ringScript.sml | 344 prod: 'a monoid (* monoid and group share the same type *) 2435 (* This export is very bad, same as conversion. *)
|
/seL4-l4v-master/HOL4/examples/algebra/field/ |
H A D | fieldScript.sml | 56 (* Data type (same as ring): 502 (* Field and Ring share the same type. *)
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | Z3_ProofReplay.sml | 910 future uses of the same proof ID merely require a lookup in the
|
/seL4-l4v-master/HOL4/src/IndDef/Manual/ |
H A D | paper.tex | 544 the terms that occur at these positions must be the same variables given in the
|
/seL4-l4v-master/HOL4/src/emit/ |
H A D | basis_emitScript.sml | 354 (* Map 0 and ZERO to the same thing in generated ML. *)
|
/seL4-l4v-master/HOL4/src/quotient/examples/lambda/ |
H A D | alphaScript.sml | 56 (* the variables must each be found at the same place. *)
|
/seL4-l4v-master/HOL4/src/quotient/examples/sigma/ |
H A D | reductionScript.sml | 249 But the following definition is not the same as that in relationTheory. *)
|
/seL4-l4v-master/HOL4/src/unwind/ |
H A D | unwindLib.sml | 110 "bound vars do not have same name"
|
/seL4-l4v-master/HOL4/tools/mllex/ |
H A D | mllex.sml | 20 user declarations at same level as makeLexer, etc.
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | polytypicLib.sml | 401 (* Exactly the same as Prim.prove_rec_fn_exists but performs checking on *) 624 " which was not universally quantified with a variable of the same type!")) 2387 (* a) Exactly the same type is visited twice *) 3116 (* Make sure we have exactly the same form as the term we were given *)
|
/seL4-l4v-master/isabelle/src/Doc/Intro/document/ |
H A D | getting.tex | 66 zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6. The same
|
/seL4-l4v-master/HOL4/examples/lambda/barendregt/ |
H A D | chap3Script.sml | 528 (* This is not the same CR as appears in There
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Intro/document/ |
H A D | getting.tex | 66 zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6. The same
|
/seL4-l4v-master/HOL4/examples/CCS/ |
H A D | StrongLawsScript.sml | 213 (* Unused recursion variables have the same behavior as `nil` *)
|
/seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
H A D | ho_proverTools.sml | 1187 val _ = assert (a_pos <> pos) (ERR "anc_frule" "same polarity")
|
/seL4-l4v-master/HOL4/examples/fun-op-sem/for/ |
H A D | forScript.sml | 1014 (* Everything above current clock gives same result if didn't time out*)
|
/seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
H A D | polyDivisionScript.sml | 979 (* Another proof of same result. *)
|
/seL4-l4v-master/HOL4/src/sort/ |
H A D | sortingScript.sml | 1245 (* PART3_FILTER - Partition is the same as filtering. *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Base.sml | 340 val cDWORD_PTR = cULONG_PTR (* Defined to be the same so I'm not sure why it's there .*)
|