/seL4-l4v-master/HOL4/Manual/Logic/ |
H A D | semantics.tex | 245 is the result of performing the same substitution across all of the 283 \PPL\index{PPlambda (same as PPLAMBDA), of LCF system@\ml{PP}$\lambda$ (same as \ml{PPLAMBDA}), of \ml{LCF} system}, since \HOL{} was 286 the same as the corresponding rule in \LCF; the code implementing this 399 The theory \theory{LOG} has the same type 893 constant $\con{c}_i$ must be the same as the type of the corresponding 1066 the introduced constants have, via their types, the same dependency on 1068 situation is the same as that discussed in the Remark in 1307 provides one way of achieving this while at the same time preserving 1501 $q$ in $M'$ are the same a [all...] |
/seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
H A D | polyDividesScript.sml | 354 (* not same as polyDivideTheory.poly_unit_property (which specifies upoly u instead of just poly u): 560 val _ = set_fixity "pdivides" (Infix(NONASSOC, 450)); (* same as relation *) 692 (* Another proof of the same theorem, with p, q interchanged. *) 713 (* Third proof of the same theorem. *) 1074 (* Original proof of the same theorem *) 1241 (* Original proof of the same theorem *) 1346 (* Original proof of the same theorem. *) 1421 (* Original proof of the same theorem. *) 1547 (* This is the same as poly_divides_mult, different proof. *) 1992 val _ = set_fixity "=~" (Infix(NONASSOC, 450)); (* same a [all...] |
/seL4-l4v-master/HOL4/examples/boyer_moore/ |
H A D | boyer_moore_specScript.sml | 38 (* The capacity to skip and produce the same solution set *)
|
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | funcCall.sml | 182 statement match, i.e. both branches have the same outputs.
|
/seL4-l4v-master/HOL4/examples/formal-languages/lambek/ |
H A D | CutFreeScript.sml | 462 >> REPEAT STRIP_TAC (* 12 subgoals, all sharing the same tacticals *) 1037 STRIP_TAC \\ (* 2 sub-goals here, sharing the same tactical *) 1042 STRIP_TAC \\ (* 2 sub-goals here, sharing the same tactical *) 1047 STRIP_TAC >| (* 2 sub-goals here, sharing the same tactical *)
|
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/ |
H A D | Scrollbar.sml | 202 (* The same values are used with different names for horizontal and vertical bars.
|
H A D | Class.sml | 194 (* We can't use the same definition of WNDCLASSEX as above because
|
H A D | FontBase.sml | 146 [CLIP_DEFAULT_PRECIS] is the same as [] i.e. zero. *)
|
/seL4-l4v-master/HOL4/src/HolSat/ |
H A D | minisatProve.sml | 156 (* same functionality for ZChaff, if installed by user *)
|
/seL4-l4v-master/HOL4/src/IndDef/ |
H A D | InductiveDefinition.sml | 31 same name, maybe it should. 575 (* Generalize definitions and theorem over given variables (all the same!) *) 860 (* All relations in a given call must have the same schematic args (if they *) 862 (* the first arguments to each relation, in the same order(!) *)
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | tcTacs.sml | 8 (* proving it equal to a term of the same form without the ^+ . *)
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | intSimps.sml | 96 Derived from code to do the same for the natural numbers, which is in
|
/seL4-l4v-master/HOL4/src/temporal/ |
H A D | examples.sml | 116 is true all the time. The same holds for PNEXT (PALWAYS a) and
|
/seL4-l4v-master/HOL4/tools/mlyacc/src/ |
H A D | shrink.sml | 108 idea is to sort the entries and place duplicates entries in the same
|
/seL4-l4v-master/HOL4/developers/ |
H A D | prehol.sml | 219 (* used to stand for "has double quote", but the same analysis is necessary
|
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | muSyntax.sml | 353 (* take f:mu and create a HOL term that replaces all :mu constants by bool names of the same type structure. 463 (* return a string term that is not the same as any in l, formed by priming mv enough times *) 470 (* rename all bound vars so that no two are the same, or clash with a free var name *) 522 (* return the max same-quantifier nesting depth of the given formula *)
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | make_sexp.ml | 404 (* (complex-rationalp #c(3 0)) ; nil, since #c(3 0) is the same as 3 *) 429 (* (complex x 0) ; same as x, for rational numbers x *) 439 (* The reader macro #C (which is the same as #c) provides a convenient way *) 441 (* #C(x y) is read to the same value as (complex x y). *)
|
H A D | sexpScript.sml | 430 (* (complex-rationalp #c(3 0)) ; nil, since #c(3 0) is the same as 3 *) 455 (* (complex x 0) ; same as x, for rational numbers x *) 465 (* The reader macro #C (which is the same as #c) provides a convenient way *) 467 (* #C(x y) is read to the same value as (complex x y). *)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Array2.sml | 52 (* Check that all the lists have the same length. *)
|
H A D | PackWord8Big.sml | 49 (* Exactly the same as Pack8Big except for the value of isBigEndian *)
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | fp.tex | 148 By the same device you can also write bounded quantifiers like 170 during proofs by simplification. The same is true for the equations in 383 same cardinality --- an impossibility. For the same reason it is not possible
|
H A D | numerics.tex | 17 Most numeric operations are overloaded: the same symbol can be 268 ML treats negative divisors in the same way, but most computer hardware 269 treats signed operands using the same rules as for multiplication. 341 for type \isa{real} have the same syntax as those for type
|
H A D | protocol.tex | 115 If Charlie tries the same attack, Alice will receive the message
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | lisp_semanticsScript.sml | 171 (* Label-defined functions share the same namespace). *)
|
/seL4-l4v-master/isabelle/src/HOL/MicroJava/document/ |
H A D | introduction.tex | 66 same data types are supported and bytecode instructions required for
|