/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ |
H A D | SIGNATURES.sml | 639 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 D | tactics.tex | 56 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 D | conv.tex | 79 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 D | HolSat.tex | 53 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 D | misc.tex | 23 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 D | quotient.tex | 952 %{\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 D | ind_rel.sml | 196 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 D | logic.tex | 150 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 D | AKSintroScript.sml | 247 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 D | FinalPolyML.sml | 42 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 D | STEScript.sml | 381 | 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 D | FOL.tex | 244 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 D | FOL.tex | 244 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 D | enumeralScript.sml | 427 (* 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 D | WeakEQScript.sml | 114 (* 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 D | quotientGroupScript.sml | 163 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 D | Theory.sml | 207 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 D | LambekScript.sml | 1910 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 D | mlibArbnum.sml | 250 raise Fail "normalised_v not same length as v"
|
H A D | mlibRewrite.sml | 214 val () = assert (j <> i) (Error "rewrite: same theorem")
|
/seL4-l4v-master/HOL4/src/proofman/ |
H A D | goalStack.sml | 252 add_string ("WARNING: goal contains variables of same name \
|
/seL4-l4v-master/HOL4/src/rational/ |
H A D | ratLib.sml | 360 (* generate the part of a product (product of the same terms and multiplicative inverses resp.) *)
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | regexpMatch.sml | 141 (* Two regexps are equivalent if they have the same language. This is *)
|
/seL4-l4v-master/HOL4/tools/mlyacc/src/ |
H A D | sigs.sml | 333 structure will contain the same information as the one passed to
|
/seL4-l4v-master/HOL4/examples/Crypto/Serpent/Reference/ |
H A D | Serpent_Reference_TransformationScript.sml | 721 (* parity check is the same as counting EVEN or ODD.
|