Searched refs:same (Results 226 - 250 of 478) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DSIGNATURES.sml639 the result list is all those structures/types with the same name. *)
642 (* Sort the items so that items with the same name are brought together.
643 A signature is not allowed to have items of the same kind with the
644 same name so this means that we are bringing together items from
646 with the same name. Discard singletons in the result. *)
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Dtactics.tex56 The proof itself, as a sequence of steps, is the same however it is found;
111 \index{proof functions (same as justifications, validations)}
321 required, the function includes as rewrites the same
393 The same proof could be constructed by forward search, starting from
469 however, is exactly the same as in the interactive proof; only the search is
1120 denote the same set (\ie\ contain the same elements).
1304 \index{proof functions (same as justifications, validations)!THEN example of@\ml{THEN} example of}
1934 discarding it at the same time,
1961 \noindent This gives the same resul
[all...]
H A Dconv.tex79 because there are relatively many of them with the same type, and
580 unless $t$ and $t'$ are the same (up to $\alpha$-conversion),
826 |- (\(n\)=\(m\)) = T \(\mbox{if \(n\) and \(m\) represent the same number}\)
H A DHolSat.tex53 Alternatively, the function {\tt SAT\_ORACLE} \index{HolSatLib!SAT\_ORACLE@\ml{SAT\_ORACLE}} has the same behaviour as {\tt SAT\_PROVE} but asserts the result of the solver without proof. The theorem thus asserted is tagged with ``{\tt{HolSatLib}}'' to indicate that it is unchecked. Since proof reconstruction can be expensive, the oracle facility can be useful during prototyping, or if proof is not required.
/seL4-l4v-master/HOL4/Manual/Description/
H A Dmisc.tex23 through the same incantation:
301 make-file target of the same name, see
475 Make-file rules are interpreted in the same way as by traditional
549 does \emph{not} do the same thing as \texttt{protect} on either Unix
570 \] turns a list of files with suffixes \texttt{.sml} into the same
657 \item[\texttt{HOLMOSMLC-C}] This variable is the same as
792 Users can use the same basic technology to ``dump'' heaps of their own.
1059 When not compact, all of a type's constructors will appear on the same line, or each will be on a separate line.
1234 The name is wrapped with \texttt{\bs{}HOLRuleName}, which by default is the same as \texttt{\bs{}textsf}.
1323 This allows one to achieve suitable alignment when other non-HOL text has been put onto the same lin
[all...]
/seL4-l4v-master/HOL4/src/quotient/Manual/
H A Dquotient.tex952 %{\it \quotient{} relation}, which is not the same as an equivalence relation.
2752 record with the same fields as above except for {\it old\_thms},
2768 are named the same as before.
2833 These are the same as the ``{\tt full}'' functions above, but
3077 has the same form as the preservation theorems of section \ref{polypreserves},
3255 the same variable {\tt zi} may be used in place of both {\tt xi} in the first
3521 lifted types, and the lifted version of the value of the same function
3769 is equal to the lifted version of the value of the same operator
3820 theorem can be proven by the user, using the same approach as for the example
3961 is the same
[all...]
/seL4-l4v-master/HOL4/src/quotient/examples/
H A Dind_rel.sml196 them to the same variable *)
346 the rules, the same variables must have the same types.) We also
443 them to the same variable *)
982 (* thx is same as thm, except with conjs in <hyp of rule> broken up *)
1718 the induct_thm (they don't need to be in the same order),
/seL4-l4v-master/HOL4/Manual/Tutorial/
H A Dlogic.tex150 When a quotation is entered into \HOL{}, the type checking algorithm uses the types of constants to infer the types of variables in the same quotation.
246 The same effect can be achieved by enclosing the symbol in parentheses.
354 The underlying constant is the same, but the printing is a clue for the user that this is equality on boolean values.
402 For example, $\ml{SPEC}\ t\ th$ will fail if $th$ is not of the form $\ml{|-\ !}x\ml{.}\cdots$ or if it is of this form but the type of $t$ is not the same as the type of $x$, or if the free variable restriction is not met.
430 Its truth conditions are thus the same as those for the
1137 same tactic to all subgoals.
/seL4-l4v-master/HOL4/examples/AKS/theories/
H A DAKSintroScript.sml247 val _ = set_fixity "intro" (Infix(NONASSOC, 450)); (* same as relation *)
1233 and the field F generated by F_p and Y is the same as the field generated by F_p and X
1300 There are two finite fields, r and r (the same).
1533 (* This result is the same as: poly_intro_X_add_c_prime_char_2, different proof. *)
1613 (* This result is the same as: poly_intro_X_add_c_prime_char_3, same proof almost. *)
/seL4-l4v-master/HOL4/polyml/basis/
H A DFinalPolyML.sml42 rehashing the table by entering values at the same time. *)
409 be the same as Bootstrap.Universal. *)
428 then (* IDE mark-up of error messages. This is actually the same as within the IDE. *)
1172 to other objects in the same directory. Objects not found must
1384 The lists should be the same length. *)
2212 (* Add the entries and print them in the same way as top-level bindings. *)
/seL4-l4v-master/HOL4/examples/STE/
H A DSTEScript.sml381 | satisfies the same STE assertion |
545 (* lattice_X1_lemma and lattice_X2_lemma state the same thing -
733 to the defining trajectory for the same formula for a given circuit model
/seL4-l4v-master/isabelle/src/Doc/Logics_ZF/document/
H A DFOL.tex244 backtracking. All the rules are derived in the same simple manner.
690 The proof script is the same as before: \isa{simp} followed by
849 Subgoal~1 yields the same countermodel as before. But each proof step has
/seL4-l4v-master/l4v/isabelle/src/Doc/Logics_ZF/document/
H A DFOL.tex244 backtracking. All the rules are derived in the same simple manner.
690 The proof script is the same as before: \isa{simp} followed by
849 Subgoal~1 yields the same countermodel as before. But each proof step has
/seL4-l4v-master/HOL4/src/finite_maps/
H A DenumeralScript.sml427 (* ordered lists of the same elements. Possiibly to no purpose, we *)
429 (* the list of the same elements as are in bt_to_set of it. Later, we *)
775 (* Now to show that building a bl from a list does the same. *)
/seL4-l4v-master/HOL4/examples/CCS/
H A DWeakEQScript.sml114 (* This cases theorem is not the same with any theorem in relationTheory *)
125 NTAC 2 DISJ2_TAC \\ (* then the rest 3 goals share the same tacticals *)
564 2. WEAK_EQUIV_cases is the same as WEAK_PROPERTY_STAR
/seL4-l4v-master/HOL4/examples/algebra/group/
H A DquotientGroupScript.sml163 val _ = set_fixity "/" (Infixl 600); (* same as "*" in arithmeticScript.sml *)
635 val _ = set_fixity "/" (Infixl 600); (* same as "*" in arithmeticScript.sml *)
1391 (3) same as (1).
/seL4-l4v-master/HOL4/src/postkernel/
H A DTheory.sml207 let fun same (node,_) = thyid_eq node n function
209 fun ins (a::rst) = if same a then addp a::rst else a::ins rst
1107 and constant definition. Almost the same as in hol88,
/seL4-l4v-master/HOL4/examples/formal-languages/lambek/
H A DLambekScript.sml1910 REPEAT STRIP_TAC (* 2 sub-goals here, same tacticals *) \\
1918 REPEAT STRIP_TAC (* 2 sub-goals here, same tacticals *) \\
1929 RES_TAC (* 2 sub-goals here, same tactical *) \\
2172 irule gentzenToNatDed \\ (* 2 sub-goals sharing the same tactical *)
/seL4-l4v-master/HOL4/src/metis/
H A DmlibArbnum.sml250 raise Fail "normalised_v not same length as v"
H A DmlibRewrite.sml214 val () = assert (j <> i) (Error "rewrite: same theorem")
/seL4-l4v-master/HOL4/src/proofman/
H A DgoalStack.sml252 add_string ("WARNING: goal contains variables of same name \
/seL4-l4v-master/HOL4/src/rational/
H A DratLib.sml360 (* generate the part of a product (product of the same terms and multiplicative inverses resp.) *)
/seL4-l4v-master/HOL4/tools/Holmake/
H A DregexpMatch.sml141 (* Two regexps are equivalent if they have the same language. This is *)
/seL4-l4v-master/HOL4/tools/mlyacc/src/
H A Dsigs.sml333 structure will contain the same information as the one passed to
/seL4-l4v-master/HOL4/examples/Crypto/Serpent/Reference/
H A DSerpent_Reference_TransformationScript.sml721 (* parity check is the same as counting EVEN or ODD.

Completed in 352 milliseconds

1234567891011>>