Searched refs:same (Results 151 - 175 of 478) sorted by relevance

1234567891011>>

/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/
H A Dfp.tex148 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 Dnumerics.tex17 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 Dprotocol.tex115 If Charlie tries the same attack, Alice will receive the message
/seL4-l4v-master/l4v/isabelle/src/HOL/MicroJava/document/
H A Dintroduction.tex66 same data types are supported and bytecode instructions required for
/seL4-l4v-master/HOL4/examples/CCS/
H A DObsCongrLawsScript.sml282 (* tau-laws for observation congruence (and the same tau-laws *)
H A DCongruenceScript.sml163 rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *)
187 rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *)
657 rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *)
686 rpt STRIP_TAC \\ (* 2 subgoals here, same tacticals *)
900 rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *)
H A DMultivariateScript.sml152 definition of EV (the set of equation variables), as the same
154 the same CCS term.
220 (* from a key list and a value list (of same length) to an alist *)
1604 (* Each solution contains the same number of CCS processes as the
1659 fs [CCS_SUBST_def, TRANS_SUM_EQ, BV_def, FV_def] \\ (* 2 subgoals, same tactics *)
1811 `IS_PROC x /\ DISJOINT (BV x) (set Xs)` is for the same case: they
2122 CONJ_TAC \\ (* s subgoals, same tactics *)
2167 CONJ_TAC \\ (* s subgoals, same tactics *)
2227 CONJ_TAC \\ (* s subgoals, same tactics *)
2247 CONJ_TAC \\ (* s subgoals, same tactic
[all...]
/seL4-l4v-master/HOL4/examples/ind_def/
H A DalgebraScript.sml267 (* if they have the same maximal traces. *)
/seL4-l4v-master/HOL4/examples/AI_tasks/
H A DmleDiophProve.sml200 Prove that the two predicates are equal on the same input
/seL4-l4v-master/HOL4/src/relation/
H A DbisimulationScript.sml295 >> RES_TAC (* 8 sub-goals here, the same last tactic *)
/seL4-l4v-master/HOL4/examples/AKS/compute/
H A DcomputeOrderScript.sml526 This is the same as:
570 If j = k, we have the same contradiction as before:
576 If j < k, this is the same as SUC j <= k.
613 (* An alternative expression of the same theorem. *)
/seL4-l4v-master/HOL4/examples/algebra/group/
H A DgroupMapScript.sml268 (* This is the same as group_homo_trans. *)
396 (* This is the same as group_iso_trans. *)
456 (* This is the same as group_iso_sym. *)
764 (* For those same as monoids, use overloading *)
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DGen_arith.sml120 non-numeral multiplicands always appear in the same order, and
/seL4-l4v-master/HOL4/src/1/
H A DTactical.sml376 * is the same as "tac", except it will fail in the cases where "tac"
381 * is the same as "ltac", except it will fail in the cases where "ltac"
443 * is the same as "tac", except that where "tac" returns a proof which is
450 * is the same as "ltac", except it will return extra goals where this is
/seL4-l4v-master/HOL4/polyml/basis/
H A DThread.sml143 (*!Test whether thread ids are the same. This is provided for backwards compatibility
256 All the threads waiting on a condition variable should pass the same mutex
305 then raise Thread "The same attribute appears more than once in the list"
433 others remain the same. *)
/seL4-l4v-master/HOL4/src/boss/
H A DbossLib.sig29 Should have the same effect as Theory.Definition.new_specification. *)
/seL4-l4v-master/HOL4/src/simp/src/
H A DsimpLib.sig167 * This is done in the same way as similar to TOP_DEPTH_CONV.
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_STATIC_LINK_AND_CASES.sml109 (* Recursive. If we pass an argument in the same position we
490 same effect. More complicated cases could be considered but
508 provided that there was an extra check for long values. N.B. the same also
551 same case to appear more than once in the list. This is not
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/binomial/
H A Dbinomial.tex335 and then to use the equation with \verb@REWRITE_TAC@ in the same way as one
377 Now that the terms appear in both sides in the same order but with different
379 the same. Again the definition of \verb@ASSOCIATIVE@ cannot be used
569 Given this lemma, which is proven by an easy tactic almost the same
939 same, using distributivity of $\times$ over $+$, associativity of $+$,
/seL4-l4v-master/HOL4/Manual/Tutorial/binomial/
H A Dbinomial.tex335 and then to use the equation with \verb@REWRITE_TAC@ in the same way as one
377 Now that the terms appear in both sides in the same order but with different
379 the same. Again the definition of \verb@ASSOCIATIVE@ cannot be used
569 Given this lemma, which is proven by an easy tactic almost the same
939 same, using distributivity of $\times$ over $+$, associativity of $+$,
/seL4-l4v-master/HOL4/examples/algebra/polynomial/
H A DpolyModuloRingScript.sml266 val _ = set_fixity "+z" (Infixl 500); (* same as + in arithmeticScript.sml *)
267 val _ = set_fixity "-z" (Infixl 500); (* same as - in arithmeticScript.sml *)
268 val _ = set_fixity "*z" (Infixl 600); (* same as * in arithmeticScript.sml *)
269 val _ = set_fixity "**z" (Infixr 700); (* same as EXP in arithmeticScript.sml, infix right *)
930 (3) x IN RM.carrier ==> x o I IN (RX / I).carrier, same as (1)
H A DpolyMapScript.sml424 val _ = set_fixity "~~r" (Infix(NONASSOC, 450)); (* same as relation *)
425 val _ = set_fixity "==r" (Infix(NONASSOC, 450)); (* same as relation *)
426 val _ = set_fixity "~f~" (Infix(NONASSOC, 450)); (* same as relation *)
427 val _ = set_fixity "=f=" (Infix(NONASSOC, 450)); (* same as relation *)
428 val _ = set_fixity "~ff~" (Infix(NONASSOC, 450)); (* same as relation *)
429 val _ = set_fixity "=ff=" (Infix(NONASSOC, 450)); (* same as relation *)
477 val _ = set_fixity "||_" (Infixl 500); (* same as + in arithmeticScript.sml *)
478 val _ = set_fixity "o_" (Infixl 500); (* same as + in arithmeticScript.sml *)
479 val _ = set_fixity ">>_" (Infixr 700); (* same as EXP in arithmeticScript.sml, infix right *)
480 val _ = set_fixity "'_" (Infixl 2000); (* same a
[all...]
/seL4-l4v-master/HOL4/examples/decidable_separationLogic/doc/
H A Dds.tex597 which obviously have the same semantics. So, $\pfequal {e_1} e_2$ and
598 $\pfequal {e_2} e_1$ are not distinguished. The same holds for $\pfunequal
741 $(e,es)$ is added to $\pi$, which has the same effect as adding $e$ to $\pi$
742 guarded by the condition that $e$ and $es$ do not evaluate to the same value,
1053 \item remove multiple occurrences of the same field index from $\Sigma$ and $\Sigma'$
1165 Do do the same proof in \HOL, one can either apply single inference rules manually or just
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/
H A DTYPEIDCODE.sml225 (* Test if we have the same type as the cached type. *)
306 | FunctionType _ => SOME(fn _ => functionCode, ~1) (* Every function has the same code. *)
779 the two arguments are the same. We don't have to
812 there's some uncertainty about whether we use the same type
932 (* eqStr assumes that all occurrences of the same single character string are shared. *)
1155 let (* Datatype. This is the same for monotype and polytypes except for the print fn. *)
/seL4-l4v-master/HOL4/examples/algebra/finitefield/
H A DffExistScript.sml345 and list univ(:'a) =~ univ(:'a) by INFINITE_A_list_BIJ_A (same cardinality)
366 so list univ(:num) =~ univ(:num) by INFINITE_A_list_BIJ_A (same cardinality)
465 INFINITE univ(:'a), which has the same cardinality as univ(:num poly), giving an injection:
1206 (* Overload on finite fields of same cardinality with isomorphic subfields *)
1210 fixity = Infix(NONASSOC, 450), (* same as relation *)
1625 Two finite fields of same cardinality are isomorphic.
1628 (1) Two finite fields of the same cardinality have the same characteristic:
1749 Thus two finite fields with same cardinality are isomorphic.
1870 Given two finite fields r, s of the same cardinalit
[all...]

Completed in 202 milliseconds

1234567891011>>