Searched refs:same (Results 276 - 300 of 478) sorted by relevance

<<11121314151617181920

/seL4-l4v-master/HOL4/examples/CCS/
H A DExpansionScript.sml62 Cases_on `u` \\ (* 2 sub-goals sharing the same tacticals *)
283 Cases_on `u` >> RES_TAC \\ (* 2 sub-goals here, same tacticals *)
/seL4-l4v-master/HOL4/src/1/
H A DTactic.sml239 * 2) rewritten so that the proof yields the same quantified var as the *
809 * (2) where multiple assumptions involve the same variable that is not in *
/seL4-l4v-master/isabelle/src/Pure/PIDE/
H A Dcommand.scala459 def same(that: Perspective): Boolean =
/seL4-l4v-master/l4v/isabelle/src/Doc/Nitpick/document/
H A Droot.tex645 Quotient types are handled in much the same way. The following fragment defines
1014 equal if and only if they lead to the same observations. For example, the two
1080 off to treat these types in the same way as plain datatypes, by approximating
1212 $'a$ and $'b$ values provided by the larger scope. Nitpick comes to the same
1283 are normally monotonic and treated as such. The same is true for record types,
1480 Now, this formula must be wrong: The same assumption occurs twice, and the
1498 Apparently, $[b, b, a, a] \notin S$, even though it has the same numbers of
2038 Specifies whether type variables with the same sort constraints should be
/seL4-l4v-master/isabelle/src/Doc/Nitpick/document/
H A Droot.tex645 Quotient types are handled in much the same way. The following fragment defines
1014 equal if and only if they lead to the same observations. For example, the two
1080 off to treat these types in the same way as plain datatypes, by approximating
1212 $'a$ and $'b$ values provided by the larger scope. Nitpick comes to the same
1283 are normally monotonic and treated as such. The same is true for record types,
1480 Now, this formula must be wrong: The same assumption occurs twice, and the
1498 Apparently, $[b, b, a, a] \notin S$, even though it has the same numbers of
2038 Specifies whether type variables with the same sort constraints should be
/seL4-l4v-master/l4v/isabelle/src/Pure/PIDE/
H A Dcommand.scala459 def same(that: Perspective): Boolean =
/seL4-l4v-master/HOL4/examples/fermat/little/
H A DpatternScript.sml247 (* Idea: only same length lists can be similar to each other. *)
762 (* Similar lists have the same order. *)
/seL4-l4v-master/HOL4/examples/fermat/twosq/
H A DinvoluteFixScript.sml182 A finite set and the set of its fixed points under any involution have cardinalities of the same parity
629 (3) same as (1).
H A DtwoSquaresScript.sml1045 (* Another proof of the same theorem, using two_sq_thm. *)
1174 (* A better proof of the same theorem *)
/seL4-l4v-master/HOL4/src/pred_set/Manual/
H A Ddescription.tex10 parallel to the much more developed \HOL\ \ml{sets} library, with the same
11 names for constants and theorems and the same form of definitions for
65 the same elements. This follows directly from the definition of the constant
711 an equality conversion of the same kind required as an argument by
1378 library theory \ml{pred\_sets} into a parent of \ml{foo}. The same effect
/seL4-l4v-master/l4v/isabelle/src/Doc/Sledgehammer/document/
H A Droot.tex402 included; the other selected facts remain the same.
658 specification with the same semantics as Sledgehammer's \textit{lam\_trans}
660 with the same semantics as Sledgehammer's \textit{type\_enc} option
904 number of facts. For SMT solvers, several slices are tried with the same options
1235 The collection of methods is roughly the same as for the \textbf{try0} command.
/seL4-l4v-master/isabelle/src/Doc/Sledgehammer/document/
H A Droot.tex402 included; the other selected facts remain the same.
658 specification with the same semantics as Sledgehammer's \textit{lam\_trans}
660 with the same semantics as Sledgehammer's \textit{type\_enc} option
904 number of facts. For SMT solvers, several slices are tried with the same options
1235 The collection of methods is roughly the same as for the \textbf{try0} command.
/seL4-l4v-master/HOL4/examples/algebra/lib/
H A DhelperNumScript.sml1873 (* Pretty version of EXP_MOD_EQN, same pattern as EXP_EQN_ALT. *)
2248 (* same as DIVIDES_EQN below *)
3234 then use the same proof for y <= z.
3393 (* binomial_add: same as SUM_SQUARED *)
3538 (* binomial_2: same as binomial_add, or SUM_SQUARED *)
/seL4-l4v-master/HOL4/examples/algebra/polynomial/
H A DpolyFieldModuloScript.sml570 val _ = set_fixity "||z" (Infixl 500); (* same as + in arithmeticScript.sml *)
571 val _ = set_fixity "oz" (Infixl 500); (* same as + in arithmeticScript.sml *)
572 val _ = set_fixity ">>z" (Infixr 700); (* same as EXP in arithmeticScript.sml, infix right *)
573 val _ = set_fixity "'z" (Infixl 2000); (* same as ' for function application *)
578 val _ = set_fixity "pdividesz" (Infix(NONASSOC, 450)); (* same as relation *)
3863 (* Another proof of the same result. *)
3931 (* Another proof of the same result. *)
5183 (3) same as (1).
5846 (4) same as (1).
5847 (5) same a
[all...]
H A DpolyRootScript.sml989 (* A better proof of the same result. *)
1107 If z is a root of (p / factor z), p just has same roots.
1352 If z is a root of (p / factor z), p just has same roots.
/seL4-l4v-master/HOL4/src/coretypes/
H A DPairRules.sml165 (* where change is true if x does not have the same structure as p. *)
167 (* where x' is of the same structure as p, created by making terms *)
2082 (* Paired stripping tactics, same as basic ones, but they use PGEN_TAC *)
/seL4-l4v-master/HOL4/examples/algebra/ring/
H A DringIdealScript.sml656 (* Characterization: x === y iff x, y in the same coset, element of (r/i) *)
967 Hence using the same argument gives <q>.carrier SUBSET <p>.carrier.
1225 By same reasoning above, apply ring_mult_comm.
/seL4-l4v-master/HOL4/src/parse/
H A Dterm_pp.sml417 the same name are rare, but it's quite reasonable for many
418 types/terms to share the same theory *)
851 vstruct list is restricted with the same term and when the
/seL4-l4v-master/HOL4/src/probability/
H A Dutil_probScript.sml1712 (* 1. for any sequence of sets, there is an increasing sequence of the same bigunion. *)
1766 the same bigunion. This lemma is needed by DYNKIN_LEMMA *)
1858 family with the same bigunion. *)
/seL4-l4v-master/HOL4/polyml/basis/
H A DPosix.sml585 (* Posix.Signal.signal is made the same as int so that we can
1023 (* file_desc and OS.IO.iodesc are the same. *)
1700 because it's now the same as int. *)
/seL4-l4v-master/HOL4/examples/dev/
H A Dcompile.sig204 (* Allows measure function to be indicated in same quotation as definition, *)
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DCFLScript.sml284 (* Other interpreters for the same synatx would be given *)
/seL4-l4v-master/HOL4/examples/dev/sw2/
H A DregAlloc.sml695 \ (e.g. all variables are not of the same type)");
/seL4-l4v-master/HOL4/src/IndDef/
H A DIndDefRules.sml216 (* then applying tac to the goal A,"!n. P[n] ==> P[SUC n] has the same *)
/seL4-l4v-master/HOL4/src/finite_maps/
H A DwotScript.sml514 (* Now the same for the strong order. WF is from relationTheory. *)

Completed in 466 milliseconds

<<11121314151617181920