/seL4-l4v-master/l4v/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/l4v/isabelle/src/HOL/MicroJava/document/ |
H A D | introduction.tex | 66 same data types are supported and bytecode instructions required for
|
/seL4-l4v-master/HOL4/examples/CCS/ |
H A D | ObsCongrLawsScript.sml | 282 (* tau-laws for observation congruence (and the same tau-laws *)
|
H A D | CongruenceScript.sml | 163 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 D | MultivariateScript.sml | 152 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 D | algebraScript.sml | 267 (* if they have the same maximal traces. *)
|
/seL4-l4v-master/HOL4/examples/AI_tasks/ |
H A D | mleDiophProve.sml | 200 Prove that the two predicates are equal on the same input
|
/seL4-l4v-master/HOL4/src/relation/ |
H A D | bisimulationScript.sml | 295 >> RES_TAC (* 8 sub-goals here, the same last tactic *)
|
/seL4-l4v-master/HOL4/examples/AKS/compute/ |
H A D | computeOrderScript.sml | 526 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 D | groupMapScript.sml | 268 (* 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 D | Gen_arith.sml | 120 non-numeral multiplicands always appear in the same order, and
|
/seL4-l4v-master/HOL4/src/1/ |
H A D | Tactical.sml | 376 * 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 D | Thread.sml | 143 (*!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 D | bossLib.sig | 29 Should have the same effect as Theory.Definition.new_specification. *)
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | simpLib.sig | 167 * This is done in the same way as similar to TOP_DEPTH_CONV.
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | CODETREE_STATIC_LINK_AND_CASES.sml | 109 (* 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 D | binomial.tex | 335 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 D | binomial.tex | 335 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 D | polyModuloRingScript.sml | 266 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 D | polyMapScript.sml | 424 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 D | ds.tex | 597 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 D | TYPEIDCODE.sml | 225 (* 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 D | ffExistScript.sml | 345 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...] |